Theorem 3impd 849

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 829	. 2 |- ((ps /\ ch /\ th) -> (ph -> ta))
4	3	com12 11	1 |- (ph -> ((ps /\ ch /\ th) -> ta))

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  3imp2 850  tgioolem 7911  iscau3 7935  iscau4 7937  caussi 7951  lmle 7957  iscms2lem3 7988  lmcau 7993  cdrci 10480  elioo1t3 10482  cnrsfin 10495  cnrscoa 10496  oefil2 10552  neifil 10553  filint2 10557  homgrf 10701  cmpmon 10714  icmpmon 10715

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 779

Copyright terms: Public domain