Theorem 3impd 1350

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3imp2  1351  3impexp  1360  po2ne  5556  oprabidw  7399  oprabid  7400  isinf  9177  infsupprpr  9421  axdc3lem4  10375  iccid  13318  difreicc  13412  fvf1tp  13721  relexpaddg  14988  issubg4  19087  rnglidlmcl  21183  reconn  24785  bcthlem2  25293  dvfsumrlim3  26008  ax5seg  29023  axcontlem4  29052  usgr2wlkneq  29841  frgrwopreg  30410  dfufd2lem  33641  cvmlift3lem4  35535  fscgr  36293  idinside  36297  brsegle  36321  seglecgr12im  36323  imp5q  36525  elicc3  36530  areacirclem1  37956  areacirclem2  37957  areacirclem4  37959  areacirc  37961  filbcmb  37988  fzmul  37989  islshpcv  39426  cvrat3  39815  4atexlem7  40448  relexpmulg  44063  gneispacess2  44499  iunconnlem2  45287  fmtnoprmfac1  47922  fmtnoprmfac2  47924  fpprwppr  48096  grimgrtri  48306  usgrgrtrirex  48307  grlimgrtri  48360  itsclc0xyqsol  49125