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  3515  elabgt  3672  tz7.7  6410  fvmptt  7036  f1oweALT  7997  wfrlem12OLD  8360  nneneq  9246  nneneqOLD  9258  pr2nelemOLD  10043  cfcoflem  10312  nnunb  12522  ndvdssub  16446  lsmcv  21143  uvcendim  21867  gsummoncoe1  22312  2ndcsep  23467  atcvat4i  32416  mdsymlem5  32426  sumdmdii  32434  dfon2lem6  35789  colineardim1  36062  bj-hbaeb2  36819  hbae-o  38904  ax12fromc15  38906  cvrat4  39445  llncvrlpln2  39559  lplncvrlvol2  39617  dihmeetlem3N  41307  naddgeoa  43407  eel2122old  44738