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  2417  hbae  2425  ceqsalt  3496  elabgt  3658  tz7.7  6394  fvmptt  7021  f1oweALT  7978  wfrlem12OLD  8342  nneneq  9236  nneneqOLD  9248  pr2nelemOLD  10039  cfcoflem  10306  nnunb  12514  ndvdssub  16406  lsmcv  21118  uvcendim  21841  gsummoncoe1  22296  2ndcsep  23451  atcvat4i  32327  mdsymlem5  32337  sumdmdii  32345  dfon2lem6  35625  colineardim1  35898  bj-hbaeb2  36536  hbae-o  38614  ax12fromc15  38616  cvrat4  39155  llncvrlpln2  39269  lplncvrlvol2  39327  dihmeetlem3N  41017  naddgeoa  43098  eel2122old  44431