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  2423  hbae  2431  ceqsalt  3470  elabgtOLD  3628  tz7.7  6332  fvmptt  6949  f1oweALT  7904  nneneq  9115  cfcoflem  10160  nnunb  12374  ndvdssub  16317  lsmcv  21076  uvcendim  21782  gsummoncoe1  22221  2ndcsep  23372  atcvat4i  32372  mdsymlem5  32382  sumdmdii  32390  dfon2lem6  35821  colineardim1  36094  bj-hbaeb2  36851  hbae-o  38941  ax12fromc15  38943  cvrat4  39481  llncvrlpln2  39595  lplncvrlvol2  39653  dihmeetlem3N  41343  naddgeoa  43426  eel2122old  44749