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  2426  hbae  2434  ceqsalt  3513  elabgt  3672  tz7.7  6412  fvmptt  7036  f1oweALT  7996  wfrlem12OLD  8359  nneneq  9244  nneneqOLD  9256  pr2nelemOLD  10041  cfcoflem  10310  nnunb  12520  ndvdssub  16443  lsmcv  21161  uvcendim  21885  gsummoncoe1  22328  2ndcsep  23483  atcvat4i  32426  mdsymlem5  32436  sumdmdii  32444  dfon2lem6  35770  colineardim1  36043  bj-hbaeb2  36801  hbae-o  38885  ax12fromc15  38887  cvrat4  39426  llncvrlpln2  39540  lplncvrlvol2  39598  dihmeetlem3N  41288  naddgeoa  43384  eel2122old  44716