Theorem 3impd 1367

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3imp2  1368  3impexp  1377  po2ne  5580  oprabidw  7480  oprabid  7481  isinf  9292  infsupprpr  9533  axdc3lem4  10568  iccid  13559  difreicc  13653  fvf1tp  13967  relexpaddg  15247  issubg4  19397  rnglidlmcl  21537  reconn  25192  bcthlem2  25690  dvfsumrlim3  26397  ax5seg  29562  axcontlem4  29591  usgr2wlkneq  30388  frgrwopreg  30970  dfufd2lem  34178  cvmlift3lem4  36288  fscgr  37053  idinside  37057  brsegle  37081  seglecgr12im  37083  imp5q  37309  elicc3  37313  areacirclem1  38887  areacirclem2  38888  areacirclem4  38890  areacirc  38892  filbcmb  38933  fzmul  38934  islshpcv  40369  cvrat3  40758  4atexlem7  41391  relexpmulg  44965  gneispacess2  45401  iunconnlem2  46171  fmtnoprmfac1  48917  fmtnoprmfac2  48919  fpprwppr  49104  grimgrtri  49314  usgrgrtrirex  49315  grlimgrtri  49368  itsclc0xyqsol  50205