Theorem 3expd 1366

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  3exp2  1367  exp516  1369  3impexp  1371  smogt  8331  axdc3lem4  10403  axcclem  10407  caubnd  15376  coprmprod  16685  catidd  17702  mulgnnass  19141  numedglnl  29301  mclsind  35880  fscgr  36390  cvrat4  40027  3dim1  40051  3dim2  40052  llnle  40102  lplnle  40124  llncvrlpln2  40141  lplncvrlvol2  40199  pmaple  40345  paddasslem14  40417  paddasslem15  40418  osumcllem11N  40550  cdlemeg46gfre  41116  cdlemk33N  41493  dia2dimlem6  41653  lclkrlem2y  42115  rexlimdv3d  43224  relexpmulnn  44245  3impexpbicom  45016  icceuelpart  48002  grlimgrtri  48585