Theorem syl7 72

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 71	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  244  syl3an3  1353  ax12  2292  hbae  2303  ax12OLD  2329  tz7.7  5666  fvmptt  6208  f1oweALT  7043  wfrlem12  7313  nneneq  8028  pr2nelem  8710  cfcoflem  8977  nnunb  11165  ndvdssub  14971  lsmcv  18962  gsummoncoe1  19495  uvcendim  20005  2ndcsep  21072  atcvat4i  28640  mdsymlem5  28650  sumdmdii  28658  dfon2lem6  30937  frrlem11  31036  colineardim1  31338  bj-hbaeb2  31993  hbae-o  33206  ax12fromc15  33208  cvrat4  33747  llncvrlpln2  33861  lplncvrlvol2  33919  dihmeetlem3N  35612  eel2122old  37964