Theorem 3expd 1355

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  1356  exp516  1358  3impexp  1360  smogt  8309  axdc3lem4  10375  axcclem  10379  caubnd  15294  coprmprod  16600  catidd  17615  mulgnnass  19051  numedglnl  29229  mclsind  35783  fscgr  36293  cvrat4  39816  3dim1  39840  3dim2  39841  llnle  39891  lplnle  39913  llncvrlpln2  39930  lplncvrlvol2  39988  pmaple  40134  paddasslem14  40206  paddasslem15  40207  osumcllem11N  40339  cdlemeg46gfre  40905  cdlemk33N  41282  dia2dimlem6  41442  lclkrlem2y  41904  rexlimdv3d  43037  relexpmulnn  44062  3impexpbicom  44833  icceuelpart  47793  grlimgrtri  48360