Theorem 3impd 847

Description: Importation deduction for triple conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3impd

Step	Hyp	Ref	Expression
1		3imp1.1	. . . 4 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	com4l 39	. . 3 |- (ps -> (ch -> (th -> (ph -> ta))))
3	2	3imp 827	. 2 |- ((ps /\ ch /\ th) -> (ph -> ta))
4	3	com12 11	1 |- (ph -> ((ps /\ ch /\ th) -> ta))

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3imp2 848  tgioolem 7914  iscau3 7938  iscau4 7940  caussi 7954  lmle 7960  iscms2lem3 7991  lmcau 7996  cdrci 10494  elioo1t3 10496  cnrsfin 10509  cnrscoa 10510  oefil2 10567  neifil 10568  filint2 10574  filint2OLD 10575  homgrf 10730  cmpmon 10743  icmpmon 10744

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