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  2421  hbae  2429  ceqsalt  3481  elabgtOLD  3639  tz7.7  6358  fvmptt  6988  f1oweALT  7951  nneneq  9170  pr2nelemOLD  9956  cfcoflem  10225  nnunb  12438  ndvdssub  16379  lsmcv  21051  uvcendim  21756  gsummoncoe1  22195  2ndcsep  23346  atcvat4i  32326  mdsymlem5  32336  sumdmdii  32344  dfon2lem6  35776  colineardim1  36049  bj-hbaeb2  36806  hbae-o  38896  ax12fromc15  38898  cvrat4  39437  llncvrlpln2  39551  lplncvrlvol2  39609  dihmeetlem3N  41299  naddgeoa  43383  eel2122old  44707