Theorem 3expd 1354

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3exp2  1355  exp516  1357  3impexp  1359  smogt  8339  axdc3lem4  10413  axcclem  10417  caubnd  15332  coprmprod  16638  catidd  17648  mulgnnass  19048  numedglnl  29078  mclsind  35564  fscgr  36075  cvrat4  39444  3dim1  39468  3dim2  39469  llnle  39519  lplnle  39541  llncvrlpln2  39558  lplncvrlvol2  39616  pmaple  39762  paddasslem14  39834  paddasslem15  39835  osumcllem11N  39967  cdlemeg46gfre  40533  cdlemk33N  40910  dia2dimlem6  41070  lclkrlem2y  41532  rexlimdv3d  42678  relexpmulnn  43705  3impexpbicom  44477  icceuelpart  47441  grlimgrtri  47999