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  8299  axdc3lem4  10363  axcclem  10367  caubnd  15282  coprmprod  16588  catidd  17603  mulgnnass  19039  numedglnl  29217  mclsind  35764  fscgr  36274  cvrat4  39703  3dim1  39727  3dim2  39728  llnle  39778  lplnle  39800  llncvrlpln2  39817  lplncvrlvol2  39875  pmaple  40021  paddasslem14  40093  paddasslem15  40094  osumcllem11N  40226  cdlemeg46gfre  40792  cdlemk33N  41169  dia2dimlem6  41329  lclkrlem2y  41791  rexlimdv3d  42925  relexpmulnn  43950  3impexpbicom  44721  icceuelpart  47682  grlimgrtri  48249