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  2453  hbae  2461  ceqsalt  3484  elabgtOLD  3627  tz7.7  6381  fvmptt  7006  f1oweALT  7973  nneneq  9205  cfcoflem  10331  nnunb  12583  ndvdssub  16559  lsmcv  21399  uvcendim  22133  gsummoncoe1  22606  2ndcsep  23758  atcvat4i  32981  mdsymlem5  32991  sumdmdii  32999  axsepg4  35784  dfon2lem6  36520  colineardim1  36796  bj-hbaeb2  37700  hbae-o  39928  ax12fromc15  39930  cvrat4  40468  llncvrlpln2  40582  lplncvrlvol2  40640  dihmeetlem3N  42330  naddgeoa  44354  eel2122old  45659