Theorem 3expd 1284

Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3expd.1	|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )

Assertion

Ref	Expression
3expd	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Proof of Theorem 3expd

Step	Hyp	Ref	Expression
1		3expd.1	. . . 4 |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
2	1	com12 32	. . 3 |- ( ( ps /\ ch /\ th ) -> ( ph -> ta ) )
3	2	3exp 1264	. 2 |- ( ps -> ( ch -> ( th -> ( ph -> ta ) ) ) )
4	3	com4r 94	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ w3a 1037

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3exp2  1285  exp516  1287  3impexp  1289  smogt  7464  axdc3lem4  9275  axcclem  9279  caubnd  14098  coprmprod  15375  catidd  16341  mulgnnass  17576  mulgnnassOLD  17577  numedglnl  26039  mclsind  31467  fscgr  32187  cvrat4  34729  3dim1  34753  3dim2  34754  llnle  34804  lplnle  34826  llncvrlpln2  34843  lplncvrlvol2  34901  pmaple  35047  paddasslem14  35119  paddasslem15  35120  osumcllem11N  35252  cdlemeg46gfre  35820  cdlemk33N  36197  dia2dimlem6  36358  lclkrlem2y  36820  relexpmulnn  38001  3impexpbicom  38685  icceuelpart  41372