Theorem 3expd 1354

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 1119	. 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3exp2  1355  exp516  1357  3impexp  1359  smogt  8295  axdc3lem4  10353  axcclem  10357  caubnd  15270  coprmprod  16576  catidd  17590  mulgnnass  19026  numedglnl  29126  mclsind  35637  fscgr  36147  cvrat4  39565  3dim1  39589  3dim2  39590  llnle  39640  lplnle  39662  llncvrlpln2  39679  lplncvrlvol2  39737  pmaple  39883  paddasslem14  39955  paddasslem15  39956  osumcllem11N  40088  cdlemeg46gfre  40654  cdlemk33N  41031  dia2dimlem6  41191  lclkrlem2y  41653  rexlimdv3d  42803  relexpmulnn  43829  3impexpbicom  44600  icceuelpart  47563  grlimgrtri  48130