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  2458  hbae  2466  ceqsalt  3491  elabgtOLD  3635  tz7.7  6393  fvmptt  7017  f1oweALT  7978  nneneq  9200  cfcoflem  10274  nnunb  12518  ndvdssub  16492  lsmcv  21302  uvcendim  22034  gsummoncoe1  22505  2ndcsep  23653  atcvat4i  32786  mdsymlem5  32796  sumdmdii  32804  axsepg4  35580  dfon2lem6  36299  colineardim1  36574  bj-hbaeb2  37494  hbae-o  39718  ax12fromc15  39720  cvrat4  40258  llncvrlpln2  40372  lplncvrlvol2  40430  dihmeetlem3N  42120  naddgeoa  44162  eel2122old  45467