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  257  ax12  2441  hbae  2449  tz7.7  6211  fvmptt  6782  f1oweALT  7667  wfrlem12  7960  nneneq  8694  pr2nelem  9424  cfcoflem  9688  nnunb  11887  ndvdssub  15754  lsmcv  19907  gsummoncoe1  20466  uvcendim  20985  2ndcsep  22061  atcvat4i  30168  mdsymlem5  30178  sumdmdii  30186  dfon2lem6  33028  colineardim1  33517  bj-hbaeb2  34136  hbae-o  36033  ax12fromc15  36035  cvrat4  36573  llncvrlpln2  36687  lplncvrlvol2  36745  dihmeetlem3N  38435  eel2122old  41045