Theorem 3expd 1355

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  3exp2  1356  exp516  1358  3impexp  1360  smogt  8307  axdc3lem4  10375  axcclem  10379  caubnd  15321  coprmprod  16630  catidd  17646  mulgnnass  19085  numedglnl  29213  mclsind  35752  fscgr  36262  cvrat4  39889  3dim1  39913  3dim2  39914  llnle  39964  lplnle  39986  llncvrlpln2  40003  lplncvrlvol2  40061  pmaple  40207  paddasslem14  40279  paddasslem15  40280  osumcllem11N  40412  cdlemeg46gfre  40978  cdlemk33N  41355  dia2dimlem6  41515  lclkrlem2y  41977  rexlimdv3d  43115  relexpmulnn  44136  3impexpbicom  44907  icceuelpart  47896  grlimgrtri  48479