Theorem 3impd 1361

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

Hypothesis

Ref	Expression
3imp1.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
3impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Proof of Theorem 3impd

Step	Hyp	Ref	Expression
1		3imp1.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4l 92	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	3imp 1122	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3imp2  1362  3impexp  1371  po2ne  5567  oprabidw  7421  oprabid  7422  isinf  9202  infsupprpr  9445  axdc3lem4  10403  iccid  13387  difreicc  13481  fvf1tp  13792  relexpaddg  15059  issubg4  19177  rnglidlmcl  21273  reconn  24876  bcthlem2  25374  dvfsumrlim3  26082  ax5seg  29095  axcontlem4  29124  usgr2wlkneq  29912  frgrwopreg  30481  dfufd2lem  33705  cvmlift3lem4  35632  fscgr  36390  idinside  36394  brsegle  36418  seglecgr12im  36420  imp5q  36632  elicc3  36637  areacirclem1  38167  areacirclem2  38168  areacirclem4  38170  areacirc  38172  filbcmb  38199  fzmul  38200  islshpcv  39637  cvrat3  40026  4atexlem7  40659  relexpmulg  44246  gneispacess2  44682  iunconnlem2  45470  fmtnoprmfac1  48134  fmtnoprmfac2  48136  fpprwppr  48321  grimgrtri  48531  usgrgrtrirex  48532  grlimgrtri  48585  itsclc0xyqsol  49350