Theorem 3expd 1351

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3exp2  1352  exp516  1354  3impexp  1356  smogt  8371  axdc3lem4  10452  axcclem  10456  caubnd  15311  coprmprod  16604  catidd  17630  mulgnnass  19027  numedglnl  28669  mclsind  34857  fscgr  35354  cvrat4  38619  3dim1  38643  3dim2  38644  llnle  38694  lplnle  38716  llncvrlpln2  38733  lplncvrlvol2  38791  pmaple  38937  paddasslem14  39009  paddasslem15  39010  osumcllem11N  39142  cdlemeg46gfre  39708  cdlemk33N  40085  dia2dimlem6  40245  lclkrlem2y  40707  rexlimdv3d  41725  relexpmulnn  42764  3impexpbicom  43544  icceuelpart  46404