Theorem 3expd 1350

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3exp2  1351  exp516  1353  3impexp  1355  smogt  8019  axdc3lem4  9918  axcclem  9922  caubnd  14771  coprmprod  16062  catidd  17014  mulgnnass  18334  numedglnl  27041  mclsind  33052  fscgr  33957  cvrat4  37045  3dim1  37069  3dim2  37070  llnle  37120  lplnle  37142  llncvrlpln2  37159  lplncvrlvol2  37217  pmaple  37363  paddasslem14  37435  paddasslem15  37436  osumcllem11N  37568  cdlemeg46gfre  38134  cdlemk33N  38511  dia2dimlem6  38671  lclkrlem2y  39133  rexlimdv3d  40025  relexpmulnn  40811  3impexpbicom  41586  icceuelpart  44349