Theorem 3expd 1353

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 1087

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 1089

This theorem is referenced by:  3exp2  1354  exp516  1356  3impexp  1358  smogt  8423  axdc3lem4  10522  axcclem  10526  caubnd  15407  coprmprod  16708  catidd  17738  mulgnnass  19149  numedglnl  29179  mclsind  35538  fscgr  36044  cvrat4  39400  3dim1  39424  3dim2  39425  llnle  39475  lplnle  39497  llncvrlpln2  39514  lplncvrlvol2  39572  pmaple  39718  paddasslem14  39790  paddasslem15  39791  osumcllem11N  39923  cdlemeg46gfre  40489  cdlemk33N  40866  dia2dimlem6  41026  lclkrlem2y  41488  rexlimdv3d  42639  relexpmulnn  43671  3impexpbicom  44450  icceuelpart  47310  grlimgrtri  47820