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  8379  axdc3lem4  10465  axcclem  10469  caubnd  15375  coprmprod  16678  catidd  17690  mulgnnass  19090  numedglnl  29069  mclsind  35538  fscgr  36044  cvrat4  39408  3dim1  39432  3dim2  39433  llnle  39483  lplnle  39505  llncvrlpln2  39522  lplncvrlvol2  39580  pmaple  39726  paddasslem14  39798  paddasslem15  39799  osumcllem11N  39931  cdlemeg46gfre  40497  cdlemk33N  40874  dia2dimlem6  41034  lclkrlem2y  41496  rexlimdv3d  42653  relexpmulnn  43680  3impexpbicom  44453  icceuelpart  47398  grlimgrtri  47956