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  2453  hbae  2461  ceqsalt  3486  elabgtOLD  3632  tz7.7  6368  fvmptt  6992  f1oweALT  7949  nneneq  9170  cfcoflem  10226  nnunb  12474  ndvdssub  16426  lsmcv  21191  uvcendim  21879  gsummoncoe1  22351  2ndcsep  23499  atcvat4i  32546  mdsymlem5  32556  sumdmdii  32564  axsepg4  35403  dfon2lem6  36100  colineardim1  36375  bj-hbaeb2  37267  hbae-o  39491  ax12fromc15  39493  cvrat4  40031  llncvrlpln2  40145  lplncvrlvol2  40203  dihmeetlem3N  41893  naddgeoa  43935  eel2122old  45257