Theorem 3expd 1352

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3exp2  1353  exp516  1355  3impexp  1357  smogt  8373  axdc3lem4  10454  axcclem  10458  caubnd  15312  coprmprod  16605  catidd  17631  mulgnnass  19032  numedglnl  28837  mclsind  35025  fscgr  35522  cvrat4  38778  3dim1  38802  3dim2  38803  llnle  38853  lplnle  38875  llncvrlpln2  38892  lplncvrlvol2  38950  pmaple  39096  paddasslem14  39168  paddasslem15  39169  osumcllem11N  39301  cdlemeg46gfre  39867  cdlemk33N  40244  dia2dimlem6  40404  lclkrlem2y  40866  rexlimdv3d  41884  relexpmulnn  42923  3impexpbicom  43703  icceuelpart  46563