Theorem 3imp1 846

Description: Importation to left triple conjunction.

Hypothesis

Ref	Expression
3imp1.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
3imp1	|- (((ph /\ ps /\ ch) /\ th) -> ta)

Proof of Theorem 3imp1

Step	Hyp	Ref	Expression
1		3imp1.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	3imp 827	. 2 |- ((ph /\ ps /\ ch) -> (th -> ta))
3	2	imp 350	1 |- (((ph /\ ps /\ ch) /\ th) -> ta)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  fvco 3774  divasst 5741  lemul1it 5837  divexpt 6599  expmwordit 6606  expnbndt 6654  expcnvlem6 7232  cnpco 7769  cnconst 7780  bl2in 7843  lmuni 7951  nvcnpi3 8422  nvcnpi4 8423  homco1t 9727  homulasst 9728  hoadddirt 9730  homco2t 9901  and4as 10432  and4com 10433  11st22nd 10458  homindlem3 10551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain