Theorem 3expd 1370

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3exp2  1371  exp516  1373  3impexp  1375  smogt  8350  axdc3lem4  10433  axcclem  10437  caubnd  15406  coprmprod  16715  catidd  17732  mulgnnass  19171  unichnlidl  21336  numedglnl  29431  mclsind  35957  fscgr  36467  cvrat4  40102  3dim1  40126  3dim2  40127  llnle  40177  lplnle  40199  llncvrlpln2  40216  lplncvrlvol2  40274  pmaple  40420  paddasslem14  40492  paddasslem15  40493  osumcllem11N  40625  cdlemeg46gfre  41191  cdlemk33N  41568  dia2dimlem6  41728  lclkrlem2y  42190  rexlimdv3d  43299  relexpmulnn  44320  3impexpbicom  45074  icceuelpart  48067  grlimgrtri  48650