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  254  ax12  2423  hbae  2431  tz7.7  6292  fvmptt  6895  f1oweALT  7815  wfrlem12OLD  8151  nneneq  8992  nneneqOLD  9004  pr2nelem  9760  cfcoflem  10028  nnunb  12229  ndvdssub  16118  lsmcv  20403  uvcendim  21054  gsummoncoe1  21475  2ndcsep  22610  atcvat4i  30759  mdsymlem5  30769  sumdmdii  30777  dfon2lem6  33764  colineardim1  34363  bj-hbaeb2  35001  hbae-o  36917  ax12fromc15  36919  cvrat4  37457  llncvrlpln2  37571  lplncvrlvol2  37629  dihmeetlem3N  39319  eel2122old  42338