Theorem 3expd 1352

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 1118	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3exp2  1353  exp516  1355  3impexp  1357  smogt  8198  axdc3lem4  10209  axcclem  10213  caubnd  15070  coprmprod  16366  catidd  17389  mulgnnass  18738  numedglnl  27514  mclsind  33532  fscgr  34382  cvrat4  37457  3dim1  37481  3dim2  37482  llnle  37532  lplnle  37554  llncvrlpln2  37571  lplncvrlvol2  37629  pmaple  37775  paddasslem14  37847  paddasslem15  37848  osumcllem11N  37980  cdlemeg46gfre  38546  cdlemk33N  38923  dia2dimlem6  39083  lclkrlem2y  39545  rexlimdv3d  40505  relexpmulnn  41317  3impexpbicom  42099  icceuelpart  44888