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  8297  axdc3lem4  10366  axcclem  10370  caubnd  15284  coprmprod  16590  catidd  17604  mulgnnass  19006  numedglnl  29107  mclsind  35545  fscgr  36056  cvrat4  39425  3dim1  39449  3dim2  39450  llnle  39500  lplnle  39522  llncvrlpln2  39539  lplncvrlvol2  39597  pmaple  39743  paddasslem14  39815  paddasslem15  39816  osumcllem11N  39948  cdlemeg46gfre  40514  cdlemk33N  40891  dia2dimlem6  41051  lclkrlem2y  41513  rexlimdv3d  42659  relexpmulnn  43685  3impexpbicom  44457  icceuelpart  47424  grlimgrtri  47991