Theorem 3expd 1276

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 1256	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
4	3	com4r 92	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3exp2  1277  exp516  1279  3impexp  1281  smogt  7351  axdc3lem4  9158  axcclem  9162  caubnd  13946  coprmprod  15213  catidd  16164  mulgnnass  17399  mulgnnassOLD  17400  mclsind  30721  fscgr  31357  cvrat4  33747  3dim1  33771  3dim2  33772  llnle  33822  lplnle  33844  llncvrlpln2  33861  lplncvrlvol2  33919  pmaple  34065  paddasslem14  34137  paddasslem15  34138  osumcllem11N  34270  cdlemeg46gfre  34838  cdlemk33N  35215  dia2dimlem6  35376  lclkrlem2y  35838  relexpmulnn  37020  3impexpbicom  37706  icceuelpart  39974