Theorem 3expd 1372

Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3expd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
3expd	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem 3expd

Step	Hyp	Ref	Expression
1		3expd.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
2	1	com12 33	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
3	2	3exp 1137	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
4	3	com4r 95	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:  3exp2  1373  exp516  1375  3impexp  1377  smogt  8368  axdc3lem4  10524  axcclem  10528  caubnd  15519  coprmprod  16829  catidd  17847  mulgnnass  19312  unichnlidl  21509  numedglnl  29715  mclsind  36314  fscgr  36825  cvrat4  40480  3dim1  40504  3dim2  40505  llnle  40555  lplnle  40577  llncvrlpln2  40594  lplncvrlvol2  40652  pmaple  40798  paddasslem14  40870  paddasslem15  40871  osumcllem11N  41003  cdlemeg46gfre  41569  cdlemk33N  41946  dia2dimlem6  42106  lclkrlem2y  42568  rexlimdv3d  43673  relexpmulnn  44694  3impexpbicom  45448  icceuelpart  48487  grlimgrtri  49070