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  8356  axdc3lem4  10455  axcclem  10459  caubnd  15446  coprmprod  16751  catidd  17768  mulgnnass  19232  unichnlidl  21425  numedglnl  29601  mclsind  36149  fscgr  36660  cvrat4  40316  3dim1  40340  3dim2  40341  llnle  40391  lplnle  40413  llncvrlpln2  40430  lplncvrlvol2  40488  pmaple  40634  paddasslem14  40706  paddasslem15  40707  osumcllem11N  40839  cdlemeg46gfre  41405  cdlemk33N  41782  dia2dimlem6  41942  lclkrlem2y  42404  rexlimdv3d  43528  relexpmulnn  44549  3impexpbicom  45303  icceuelpart  48336  grlimgrtri  48919