Theorem 3expd 1372

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 33	. . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏))
3	2	3exp 1137	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
4	3	com4r 95	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  3exp2  1373  exp516  1375  3impexp  1377  smogt  8350  axdc3lem4  10441  axcclem  10445  caubnd  15415  coprmprod  16723  catidd  17740  mulgnnass  19179  unichnlidl  21371  numedglnl  29503  mclsind  36070  fscgr  36580  cvrat4  40245  3dim1  40269  3dim2  40270  llnle  40320  lplnle  40342  llncvrlpln2  40359  lplncvrlvol2  40417  pmaple  40563  paddasslem14  40635  paddasslem15  40636  osumcllem11N  40768  cdlemeg46gfre  41334  cdlemk33N  41711  dia2dimlem6  41871  lclkrlem2y  42333  rexlimdv3d  43442  relexpmulnn  44463  3impexpbicom  45217  icceuelpart  48213  grlimgrtri  48796