Theorem syl7 75

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 74	1 ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl7bi  258  ax12  2452  hbae  2460  ceqsalt  3483  elabgtOLD  3626  tz7.7  6388  fvmptt  7014  f1oweALT  7984  nneneq  9224  cfcoflem  10353  nnunb  12605  ndvdssub  16584  lsmcv  21424  uvcendim  22158  gsummoncoe1  22631  2ndcsep  23783  atcvat4i  33004  mdsymlem5  33014  sumdmdii  33022  axsepg4  35867  dfon2lem6  36642  colineardim1  36918  bj-hbaeb2  37822  hbae-o  40053  ax12fromc15  40055  cvrat4  40593  llncvrlpln2  40707  lplncvrlvol2  40765  dihmeetlem3N  42455  naddgeoa  44489  eel2122old  45793