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  2455  hbae  2463  ceqsalt  3488  elabgtOLD  3633  tz7.7  6388  fvmptt  7012  f1oweALT  7970  nneneq  9191  cfcoflem  10257  nnunb  12501  ndvdssub  16468  lsmcv  21246  uvcendim  21978  gsummoncoe1  22449  2ndcsep  23597  atcvat4i  32727  mdsymlem5  32737  sumdmdii  32745  axsepg4  35534  dfon2lem6  36256  colineardim1  36531  bj-hbaeb2  37431  hbae-o  39655  ax12fromc15  39657  cvrat4  40195  llncvrlpln2  40309  lplncvrlvol2  40367  dihmeetlem3N  42057  naddgeoa  44101  eel2122old  45406