Theorem 3impd 1346

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

Syntax hints:   → wi 4   ∧ w3a 1085

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

This theorem is referenced by:  3imp2  1347  3impexp  1356  po2ne  5510  oprabidw  7286  oprabid  7287  wfrlem12OLD  8122  isinf  8965  infsupprpr  9193  axdc3lem4  10140  iccid  13053  difreicc  13145  relexpaddg  14692  issubg4  18689  reconn  23897  bcthlem2  24394  dvfsumrlim3  25102  ax5seg  27209  axcontlem4  27238  usgr2wlkneq  28025  frgrwopreg  28588  cvmlift3lem4  33184  fscgr  34309  idinside  34313  brsegle  34337  seglecgr12im  34339  imp5q  34428  elicc3  34433  areacirclem1  35792  areacirclem2  35793  areacirclem4  35795  areacirc  35797  filbcmb  35825  fzmul  35826  islshpcv  36994  cvrat3  37383  4atexlem7  38016  relexpmulg  41207  gneispacess2  41645  iunconnlem2  42444  fmtnoprmfac1  44905  fmtnoprmfac2  44907  fpprwppr  45079  itsclc0xyqsol  46002