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  8287  axdc3lem4  10344  axcclem  10348  caubnd  15266  coprmprod  16572  catidd  17586  mulgnnass  19022  numedglnl  29123  mclsind  35612  fscgr  36120  cvrat4  39488  3dim1  39512  3dim2  39513  llnle  39563  lplnle  39585  llncvrlpln2  39602  lplncvrlvol2  39660  pmaple  39806  paddasslem14  39878  paddasslem15  39879  osumcllem11N  40011  cdlemeg46gfre  40577  cdlemk33N  40954  dia2dimlem6  41114  lclkrlem2y  41576  rexlimdv3d  42722  relexpmulnn  43748  3impexpbicom  44519  icceuelpart  47473  grlimgrtri  48040