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  257  ax12  2439  hbae  2447  tz7.7  6210  fvmptt  6781  f1oweALT  7665  wfrlem12  7958  nneneq  8692  pr2nelem  9422  cfcoflem  9686  nnunb  11885  ndvdssub  15752  lsmcv  19905  gsummoncoe1  20464  uvcendim  20983  2ndcsep  22059  atcvat4i  30166  mdsymlem5  30176  sumdmdii  30184  dfon2lem6  33026  colineardim1  33515  bj-hbaeb2  34134  hbae-o  36031  ax12fromc15  36033  cvrat4  36571  llncvrlpln2  36685  lplncvrlvol2  36743  dihmeetlem3N  38433  eel2122old  41042