MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl7 Structured version   Visualization version   GIF version

Theorem syl7 71
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
StepHypRef Expression
1 syl7.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
3 syl7.2 . 2 (𝜒 → (𝜃 → (𝜓𝜏)))
42, 3syl5d 70 1 (𝜒 → (𝜃 → (𝜑𝜏)))
Colors of variables: wff setvar class
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  243  syl3an3  1352  ax12  2287  hbae  2298  ax12OLD  2324  tz7.7  5648  fvmptt  6189  f1oweALT  7016  wfrlem12  7286  nneneq  8001  pr2nelem  8683  cfcoflem  8950  nnunb  11131  ndvdssub  14913  lsmcv  18904  gsummoncoe1  19437  uvcendim  19943  2ndcsep  21010  atcvat4i  28442  mdsymlem5  28452  sumdmdii  28460  dfon2lem6  30739  frrlem11  30838  colineardim1  31140  bj-hbaeb2  31802  hbae-o  33005  ax12fromc15  33007  cvrat4  33546  llncvrlpln2  33660  lplncvrlvol2  33718  dihmeetlem3N  35411  eel2122old  37763
  Copyright terms: Public domain W3C validator