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  10448  axcclem  10452  caubnd  15430  coprmprod  16737  catidd  17754  mulgnnass  19199  unichnlidl  21392  numedglnl  29525  mclsind  36075  fscgr  36585  cvrat4  40250  3dim1  40274  3dim2  40275  llnle  40325  lplnle  40347  llncvrlpln2  40364  lplncvrlvol2  40422  pmaple  40568  paddasslem14  40640  paddasslem15  40641  osumcllem11N  40773  cdlemeg46gfre  41339  cdlemk33N  41716  dia2dimlem6  41876  lclkrlem2y  42338  rexlimdv3d  43447  relexpmulnn  44468  3impexpbicom  45222  icceuelpart  48218  grlimgrtri  48801