Theorem 3impd 1341

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

Syntax hints:   → wi 4   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3imp2  1342  3impexp  1351  po2ne  5377  oprabid  7047  wfrlem12  7818  isinf  8577  infsupprpr  8814  axdc3lem4  9721  iccid  12633  difreicc  12720  relexpaddg  14246  issubg4  18052  reconn  23119  bcthlem2  23611  dvfsumrlim3  24313  ax5seg  26407  axcontlem4  26436  usgr2wlkneq  27224  frgrwopreg  27794  cvmlift3lem4  32177  fscgr  33150  idinside  33154  brsegle  33178  seglecgr12im  33180  imp5q  33269  elicc3  33274  areacirclem1  34513  areacirclem2  34514  areacirclem4  34516  areacirc  34518  filbcmb  34547  fzmul  34548  islshpcv  35720  cvrat3  36109  4atexlem7  36742  relexpmulg  39540  gneispacess2  39981  iunconnlem2  40808  fmtnoprmfac1  43209  fmtnoprmfac2  43211  fpprwppr  43386  itsclc0xyqsol  44236