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  2425  hbae  2433  ceqsalt  3471  elabgtOLD  3624  tz7.7  6337  fvmptt  6955  f1oweALT  7910  nneneq  9122  cfcoflem  10170  nnunb  12384  ndvdssub  16322  lsmcv  21080  uvcendim  21786  gsummoncoe1  22224  2ndcsep  23375  atcvat4i  32379  mdsymlem5  32389  sumdmdii  32397  dfon2lem6  35851  colineardim1  36126  bj-hbaeb2  36883  hbae-o  39022  ax12fromc15  39024  cvrat4  39562  llncvrlpln2  39676  lplncvrlvol2  39734  dihmeetlem3N  41424  naddgeoa  43511  eel2122old  44834