Theorem 3impd 1345

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3imp2  1346  3impexp  1355  po2ne  5606  oprabidw  7450  oprabid  7451  wfrlem12OLD  8341  isinf  9285  isinfOLD  9286  infsupprpr  9529  axdc3lem4  10478  iccid  13404  difreicc  13496  relexpaddg  15036  issubg4  19108  rnglidlmcl  21124  reconn  24788  bcthlem2  25297  dvfsumrlim3  26012  ax5seg  28821  axcontlem4  28850  usgr2wlkneq  29642  frgrwopreg  30205  dfufd2lem  33361  cvmlift3lem4  35060  fscgr  35804  idinside  35808  brsegle  35832  seglecgr12im  35834  imp5q  35924  elicc3  35929  areacirclem1  37309  areacirclem2  37310  areacirclem4  37312  areacirc  37314  filbcmb  37341  fzmul  37342  islshpcv  38652  cvrat3  39042  4atexlem7  39675  relexpmulg  43279  gneispacess2  43715  iunconnlem2  44513  fmtnoprmfac1  47039  fmtnoprmfac2  47041  fpprwppr  47213  itsclc0xyqsol  48024