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  8379  axdc3lem4  10535  axcclem  10539  caubnd  15532  coprmprod  16842  catidd  17860  mulgnnass  19325  unichnlidl  21522  numedglnl  29728  mclsind  36422  fscgr  36938  cvrat4  40594  3dim1  40618  3dim2  40619  llnle  40669  lplnle  40691  llncvrlpln2  40708  lplncvrlvol2  40766  pmaple  40912  paddasslem14  40984  paddasslem15  40985  osumcllem11N  41117  cdlemeg46gfre  41683  cdlemk33N  42060  dia2dimlem6  42220  lclkrlem2y  42682  rexlimdv3d  43787  relexpmulnn  44803  3impexpbicom  45557  icceuelpart  48612  grlimgrtri  49195