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  8336  axdc3lem4  10406  axcclem  10410  caubnd  15325  coprmprod  16631  catidd  17641  mulgnnass  19041  numedglnl  29071  mclsind  35557  fscgr  36068  cvrat4  39437  3dim1  39461  3dim2  39462  llnle  39512  lplnle  39534  llncvrlpln2  39551  lplncvrlvol2  39609  pmaple  39755  paddasslem14  39827  paddasslem15  39828  osumcllem11N  39960  cdlemeg46gfre  40526  cdlemk33N  40903  dia2dimlem6  41063  lclkrlem2y  41525  rexlimdv3d  42671  relexpmulnn  43698  3impexpbicom  44470  icceuelpart  47437  grlimgrtri  47995