Theorem 3expd 1349

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3exp2  1350  exp516  1352  3impexp  1354  smogt  8003  axdc3lem4  9874  axcclem  9878  caubnd  14717  coprmprod  16004  catidd  16950  mulgnnass  18261  numedglnl  26928  mclsind  32817  fscgr  33541  cvrat4  36578  3dim1  36602  3dim2  36603  llnle  36653  lplnle  36675  llncvrlpln2  36692  lplncvrlvol2  36750  pmaple  36896  paddasslem14  36968  paddasslem15  36969  osumcllem11N  37101  cdlemeg46gfre  37667  cdlemk33N  38044  dia2dimlem6  38204  lclkrlem2y  38666  rexlimdv3d  39278  relexpmulnn  40052  3impexpbicom  40811  icceuelpart  43595