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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3exp2  1355  exp516  1357  3impexp  1359  smogt  8407  axdc3lem4  10493  axcclem  10497  caubnd  15397  coprmprod  16698  catidd  17723  mulgnnass  19127  numedglnl  29161  mclsind  35575  fscgr  36081  cvrat4  39445  3dim1  39469  3dim2  39470  llnle  39520  lplnle  39542  llncvrlpln2  39559  lplncvrlvol2  39617  pmaple  39763  paddasslem14  39835  paddasslem15  39836  osumcllem11N  39968  cdlemeg46gfre  40534  cdlemk33N  40911  dia2dimlem6  41071  lclkrlem2y  41533  rexlimdv3d  42694  relexpmulnn  43722  3impexpbicom  44500  icceuelpart  47423  grlimgrtri  47963