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  2427  hbae  2435  ceqsalt  3494  elabgt  3651  tz7.7  6378  fvmptt  7006  f1oweALT  7971  wfrlem12OLD  8334  nneneq  9220  pr2nelemOLD  10017  cfcoflem  10286  nnunb  12497  ndvdssub  16428  lsmcv  21102  uvcendim  21807  gsummoncoe1  22246  2ndcsep  23397  atcvat4i  32378  mdsymlem5  32388  sumdmdii  32396  dfon2lem6  35806  colineardim1  36079  bj-hbaeb2  36836  hbae-o  38921  ax12fromc15  38923  cvrat4  39462  llncvrlpln2  39576  lplncvrlvol2  39634  dihmeetlem3N  41324  naddgeoa  43418  eel2122old  44742