Theorem syl7 74

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

Ref	Expression
syl7.1	⊢ (𝜑 → 𝜓)
syl7.2	⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))

Assertion

Ref	Expression
syl7	⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3		syl7.2	. 2 ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))
4	2, 3	syl5d 73	1 ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl7bi  255  ax12  2427  hbae  2435  ceqsalt  3474  elabgtOLD  3627  tz7.7  6343  fvmptt  6961  f1oweALT  7916  nneneq  9130  cfcoflem  10182  nnunb  12397  ndvdssub  16336  lsmcv  21096  uvcendim  21802  gsummoncoe1  22252  2ndcsep  23403  atcvat4i  32472  mdsymlem5  32482  sumdmdii  32490  dfon2lem6  35980  colineardim1  36255  bj-hbaeb2  37019  hbae-o  39159  ax12fromc15  39161  cvrat4  39699  llncvrlpln2  39813  lplncvrlvol2  39871  dihmeetlem3N  41561  naddgeoa  43632  eel2122old  44954