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  8300  axdc3lem4  10366  axcclem  10370  caubnd  15312  coprmprod  16621  catidd  17637  mulgnnass  19076  numedglnl  29227  mclsind  35768  fscgr  36278  cvrat4  39903  3dim1  39927  3dim2  39928  llnle  39978  lplnle  40000  llncvrlpln2  40017  lplncvrlvol2  40075  pmaple  40221  paddasslem14  40293  paddasslem15  40294  osumcllem11N  40426  cdlemeg46gfre  40992  cdlemk33N  41369  dia2dimlem6  41529  lclkrlem2y  41991  rexlimdv3d  43129  relexpmulnn  44154  3impexpbicom  44925  icceuelpart  47908  grlimgrtri  48491