Theorem syl7 74

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 73	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  255  ax12  2428  hbae  2436  ceqsalt  3464  elabgtOLD  3616  tz7.7  6343  fvmptt  6962  f1oweALT  7918  nneneq  9133  cfcoflem  10185  nnunb  12424  ndvdssub  16369  lsmcv  21131  uvcendim  21837  gsummoncoe1  22283  2ndcsep  23434  atcvat4i  32483  mdsymlem5  32493  sumdmdii  32501  dfon2lem6  35984  colineardim1  36259  bj-hbaeb2  37141  hbae-o  39363  ax12fromc15  39365  cvrat4  39903  llncvrlpln2  40017  lplncvrlvol2  40075  dihmeetlem3N  41765  naddgeoa  43840  eel2122old  45162