Theorem 3expd 1350

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3exp2  1351  exp516  1353  3impexp  1355  smogt  7987  axdc3lem4  9864  axcclem  9868  caubnd  14710  coprmprod  15995  catidd  16943  mulgnnass  18254  numedglnl  26937  mclsind  32930  fscgr  33654  cvrat4  36739  3dim1  36763  3dim2  36764  llnle  36814  lplnle  36836  llncvrlpln2  36853  lplncvrlvol2  36911  pmaple  37057  paddasslem14  37129  paddasslem15  37130  osumcllem11N  37262  cdlemeg46gfre  37828  cdlemk33N  38205  dia2dimlem6  38365  lclkrlem2y  38827  rexlimdv3d  39624  relexpmulnn  40410  3impexpbicom  41185  icceuelpart  43953