Theorem 3impd 1281

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

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 92	. . 3 |- ( ps -> ( ch -> ( th -> ( ph -> ta ) ) ) )
3	2	3imp 1256	. 2 |- ( ( ps /\ ch /\ th ) -> ( ph -> ta ) )
4	3	com12 32	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:  3imp2  1282  3impexp  1289  oprabid  6677  wfrlem12  7426  isinf  8173  axdc3lem4  9275  iccid  12220  difreicc  12304  relexpaddg  13793  issubg4  17613  reconn  22631  bcthlem2  23122  dvfsumrlim3  23796  ax5seg  25818  axcontlem4  25847  usgr2wlkneq  26652  frgrwopreg  27187  cvmlift3lem4  31304  frrlem11  31792  fscgr  32187  idinside  32191  brsegle  32215  seglecgr12im  32217  imp5q  32306  elicc3  32311  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirc  33505  filbcmb  33535  fzmul  33537  islshpcv  34340  cvrat3  34728  4atexlem7  35361  relexpmulg  38002  gneispacess2  38444  iunconnlem2  39171  fmtnoprmfac1  41477  fmtnoprmfac2  41479