Theorem 3expd 1360

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3exp2  1361  exp516  1363  3impexp  1365  smogt  8304  axdc3lem4  10373  axcclem  10377  caubnd  15319  coprmprod  16628  catidd  17644  mulgnnass  19083  numedglnl  29238  mclsind  35805  fscgr  36315  cvrat4  39942  3dim1  39966  3dim2  39967  llnle  40017  lplnle  40039  llncvrlpln2  40056  lplncvrlvol2  40114  pmaple  40260  paddasslem14  40332  paddasslem15  40333  osumcllem11N  40465  cdlemeg46gfre  41031  cdlemk33N  41408  dia2dimlem6  41568  lclkrlem2y  42030  rexlimdv3d  43139  relexpmulnn  44160  3impexpbicom  44931  icceuelpart  47918  grlimgrtri  48501