Theorem 3expd 1372

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 33	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
3	2	3exp 1137	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
4	3	com4r 95	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3exp2  1373  exp516  1375  3impexp  1377  smogt  8413  axdc3lem4  10570  axcclem  10574  caubnd  15570  coprmprod  16880  catidd  17904  mulgnnass  19369  unichnlidl  21567  numedglnl  29779  mclsind  36543  fscgr  37060  cvrat4  40766  3dim1  40790  3dim2  40791  llnle  40841  lplnle  40863  llncvrlpln2  40880  lplncvrlvol2  40938  pmaple  41084  paddasslem14  41156  paddasslem15  41157  osumcllem11N  41289  cdlemeg46gfre  41855  cdlemk33N  42232  dia2dimlem6  42392  lclkrlem2y  42854  rexlimdv3d  43959  relexpmulnn  44970  3impexpbicom  45723  icceuelpart  48791  grlimgrtri  49374