Theorem 3expd 1351

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3exp2  1352  exp516  1354  3impexp  1356  smogt  8169  axdc3lem4  10140  axcclem  10144  caubnd  14998  coprmprod  16294  catidd  17306  mulgnnass  18653  numedglnl  27417  mclsind  33432  fscgr  34309  cvrat4  37384  3dim1  37408  3dim2  37409  llnle  37459  lplnle  37481  llncvrlpln2  37498  lplncvrlvol2  37556  pmaple  37702  paddasslem14  37774  paddasslem15  37775  osumcllem11N  37907  cdlemeg46gfre  38473  cdlemk33N  38850  dia2dimlem6  39010  lclkrlem2y  39472  rexlimdv3d  40421  relexpmulnn  41206  3impexpbicom  41988  icceuelpart  44776