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  254  ax12  2423  hbae  2431  tz7.7  6277  fvmptt  6877  f1oweALT  7788  wfrlem12OLD  8122  nneneq  8896  pr2nelem  9691  cfcoflem  9959  nnunb  12159  ndvdssub  16046  lsmcv  20318  uvcendim  20964  gsummoncoe1  21385  2ndcsep  22518  atcvat4i  30660  mdsymlem5  30670  sumdmdii  30678  dfon2lem6  33670  colineardim1  34290  bj-hbaeb2  34928  hbae-o  36844  ax12fromc15  36846  cvrat4  37384  llncvrlpln2  37498  lplncvrlvol2  37556  dihmeetlem3N  39246  eel2122old  42227