Theorem 3expd 1352

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 1118	. 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  1353  exp516  1355  3impexp  1357  smogt  8405  axdc3lem4  10490  axcclem  10494  caubnd  15393  coprmprod  16694  catidd  17724  mulgnnass  19139  numedglnl  29175  mclsind  35554  fscgr  36061  cvrat4  39425  3dim1  39449  3dim2  39450  llnle  39500  lplnle  39522  llncvrlpln2  39539  lplncvrlvol2  39597  pmaple  39743  paddasslem14  39815  paddasslem15  39816  osumcllem11N  39948  cdlemeg46gfre  40514  cdlemk33N  40891  dia2dimlem6  41051  lclkrlem2y  41513  rexlimdv3d  42670  relexpmulnn  43698  3impexpbicom  44476  icceuelpart  47360  grlimgrtri  47898