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  2421  hbae  2429  ceqsalt  3472  elabgtOLD  3630  tz7.7  6337  fvmptt  6954  f1oweALT  7914  nneneq  9130  cfcoflem  10185  nnunb  12398  ndvdssub  16338  lsmcv  21066  uvcendim  21772  gsummoncoe1  22211  2ndcsep  23362  atcvat4i  32359  mdsymlem5  32369  sumdmdii  32377  dfon2lem6  35761  colineardim1  36034  bj-hbaeb2  36791  hbae-o  38881  ax12fromc15  38883  cvrat4  39422  llncvrlpln2  39536  lplncvrlvol2  39594  dihmeetlem3N  41284  naddgeoa  43367  eel2122old  44691