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 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ w3a 1103

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

This theorem is referenced by:  3exp2  1373  exp516  1375  3impexp  1377  smogt  8355  axdc3lem4  10438  axcclem  10442  caubnd  15412  coprmprod  16720  catidd  17737  mulgnnass  19176  unichnlidl  21343  numedglnl  29475  mclsind  36043  fscgr  36553  cvrat4  40198  3dim1  40222  3dim2  40223  llnle  40273  lplnle  40295  llncvrlpln2  40312  lplncvrlvol2  40370  pmaple  40516  paddasslem14  40588  paddasslem15  40589  osumcllem11N  40721  cdlemeg46gfre  41287  cdlemk33N  41664  dia2dimlem6  41824  lclkrlem2y  42286  rexlimdv3d  43397  relexpmulnn  44418  3impexpbicom  45172  icceuelpart  48168  grlimgrtri  48751