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  258  ax12  2422  hbae  2430  tz7.7  6217  fvmptt  6816  f1oweALT  7723  wfrlem12  8044  nneneq  8807  pr2nelem  9583  cfcoflem  9851  nnunb  12051  ndvdssub  15933  lsmcv  20132  uvcendim  20763  gsummoncoe1  21179  2ndcsep  22310  atcvat4i  30432  mdsymlem5  30442  sumdmdii  30450  dfon2lem6  33434  colineardim1  34049  bj-hbaeb2  34687  hbae-o  36603  ax12fromc15  36605  cvrat4  37143  llncvrlpln2  37257  lplncvrlvol2  37315  dihmeetlem3N  39005  eel2122old  41952