Theorem 3expd 1349

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3exp2  1350  exp516  1352  3impexp  1354  smogt  7998  axdc3lem4  9869  axcclem  9873  caubnd  14712  coprmprod  15999  catidd  16945  mulgnnass  18256  numedglnl  26923  mclsind  32812  fscgr  33536  cvrat4  36573  3dim1  36597  3dim2  36598  llnle  36648  lplnle  36670  llncvrlpln2  36687  lplncvrlvol2  36745  pmaple  36891  paddasslem14  36963  paddasslem15  36964  osumcllem11N  37096  cdlemeg46gfre  37662  cdlemk33N  38039  dia2dimlem6  38199  lclkrlem2y  38661  rexlimdv3d  39273  relexpmulnn  40047  3impexpbicom  40806  icceuelpart  43590