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

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  258  ax12  2457  hbae  2465  ceqsalt  3490  elabgtOLD  3635  tz7.7  6376  fvmptt  7000  f1oweALT  7957  nneneq  9178  cfcoflem  10244  nnunb  12491  ndvdssub  16457  lsmcv  21234  uvcendim  21957  gsummoncoe1  22429  2ndcsep  23577  atcvat4i  32658  mdsymlem5  32668  sumdmdii  32676  axsepg4  35451  dfon2lem6  36149  colineardim1  36424  bj-hbaeb2  37315  hbae-o  39539  ax12fromc15  39541  cvrat4  40079  llncvrlpln2  40193  lplncvrlvol2  40251  dihmeetlem3N  41941  naddgeoa  43983  eel2122old  45291