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  3476  elabgtOLD  3629  tz7.7  6351  fvmptt  6970  f1oweALT  7926  nneneq  9142  cfcoflem  10194  nnunb  12409  ndvdssub  16348  lsmcv  21108  uvcendim  21814  gsummoncoe1  22264  2ndcsep  23415  atcvat4i  32484  mdsymlem5  32494  sumdmdii  32502  dfon2lem6  35999  colineardim1  36274  bj-hbaeb2  37060  hbae-o  39273  ax12fromc15  39275  cvrat4  39813  llncvrlpln2  39927  lplncvrlvol2  39985  dihmeetlem3N  41675  naddgeoa  43745  eel2122old  45067