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  2455  hbae  2463  ceqsalt  3487  elabgtOLD  3630  tz7.7  6406  fvmptt  7037  f1oweALT  8008  nneneq  9249  cfcoflem  10377  nnunb  12629  ndvdssub  16608  lsmcv  21449  uvcendim  22183  gsummoncoe1  22656  2ndcsep  23808  atcvat4i  33029  mdsymlem5  33039  sumdmdii  33047  axsepg4  35911  dfon2lem6  36728  colineardim1  37004  bj-hbaeb2  37908  hbae-o  40152  ax12fromc15  40154  cvrat4  40692  llncvrlpln2  40806  lplncvrlvol2  40864  dihmeetlem3N  42554  naddgeoa  44588  eel2122old  45891