Theorem 3impd 1349

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 1110	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3imp2  1350  3impexp  1359  po2ne  5565  oprabidw  7421  oprabid  7422  isinf  9214  isinfOLD  9215  infsupprpr  9464  axdc3lem4  10413  iccid  13358  difreicc  13452  fvf1tp  13758  relexpaddg  15026  issubg4  19084  rnglidlmcl  21133  reconn  24724  bcthlem2  25232  dvfsumrlim3  25947  ax5seg  28872  axcontlem4  28901  usgr2wlkneq  29693  frgrwopreg  30259  dfufd2lem  33527  cvmlift3lem4  35316  fscgr  36075  idinside  36079  brsegle  36103  seglecgr12im  36105  imp5q  36307  elicc3  36312  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirc  37714  filbcmb  37741  fzmul  37742  islshpcv  39053  cvrat3  39443  4atexlem7  40076  relexpmulg  43706  gneispacess2  44142  iunconnlem2  44931  fmtnoprmfac1  47570  fmtnoprmfac2  47572  fpprwppr  47744  grimgrtri  47952  usgrgrtrirex  47953  grlimgrtri  47999  itsclc0xyqsol  48761