Theorem 3impd 1349

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3imp2  1350  3impexp  1359  po2ne  5605  oprabidw  7440  oprabid  7441  wfrlem12OLD  8320  isinf  9260  isinfOLD  9261  infsupprpr  9499  axdc3lem4  10448  iccid  13369  difreicc  13461  relexpaddg  15000  issubg4  19025  reconn  24344  bcthlem2  24842  dvfsumrlim3  25550  ax5seg  28196  axcontlem4  28225  usgr2wlkneq  29013  frgrwopreg  29576  cvmlift3lem4  34313  fscgr  35052  idinside  35056  brsegle  35080  seglecgr12im  35082  imp5q  35197  elicc3  35202  areacirclem1  36576  areacirclem2  36577  areacirclem4  36579  areacirc  36581  filbcmb  36608  fzmul  36609  islshpcv  37923  cvrat3  38313  4atexlem7  38946  relexpmulg  42461  gneispacess2  42897  iunconnlem2  43696  fmtnoprmfac1  46233  fmtnoprmfac2  46235  fpprwppr  46407  rnglidlmcl  46748  itsclc0xyqsol  47454