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  2422  hbae  2430  ceqsalt  3484  elabgtOLD  3642  tz7.7  6361  fvmptt  6991  f1oweALT  7954  nneneq  9176  pr2nelemOLD  9963  cfcoflem  10232  nnunb  12445  ndvdssub  16386  lsmcv  21058  uvcendim  21763  gsummoncoe1  22202  2ndcsep  23353  atcvat4i  32333  mdsymlem5  32343  sumdmdii  32351  dfon2lem6  35783  colineardim1  36056  bj-hbaeb2  36813  hbae-o  38903  ax12fromc15  38905  cvrat4  39444  llncvrlpln2  39558  lplncvrlvol2  39616  dihmeetlem3N  41306  naddgeoa  43390  eel2122old  44714