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 401  df-3an 1105

This theorem is used by:  3imp2  1368  3impexp  1377  po2ne  5585  oprabidw  7441  oprabid  7442  isinf  9221  infsupprpr  9462  axdc3lem4  10441  iccid  13421  difreicc  13515  fvf1tp  13827  relexpaddg  15095  issubg4  19216  rnglidlmcl  21350  reconn  24995  bcthlem2  25493  dvfsumrlim3  26201  ax5seg  29297  axcontlem4  29326  usgr2wlkneq  30114  frgrwopreg  30683  dfufd2lem  33848  cvmlift3lem4  35822  fscgr  36580  idinside  36584  brsegle  36608  seglecgr12im  36610  imp5q  36852  elicc3  36856  areacirclem1  38387  areacirclem2  38388  areacirclem4  38390  areacirc  38392  filbcmb  38419  fzmul  38420  islshpcv  39855  cvrat3  40244  4atexlem7  40877  relexpmulg  44464  gneispacess2  44900  iunconnlem2  45671  fmtnoprmfac1  48345  fmtnoprmfac2  48347  fpprwppr  48532  grimgrtri  48742  usgrgrtrirex  48743  grlimgrtri  48796  itsclc0xyqsol  49576