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

Theorem syl7 68
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 67 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl7bi  230  syl3an3  1263  hbae  2055  equveliOLD  2089  hbae-o  2232  ax12  2234  tz7.7  4909  fvmptt  5971  f1oweALT  6784  nneneq  7720  pr2nelem  8403  cfcoflem  8673  nnunb  10816  ndvdssub  14065  lsmcv  17787  gsummoncoe1  18346  uvcendim  18882  2ndcsep  19960  atcvat4i  27316  mdsymlem5  27326  sumdmdii  27334  dfon2lem6  29220  wfrlem12  29354  frrlem11  29399  colineardim1  29711  eel2122old  33513  bj-hbaeb2  34391  cvrat4  35167  llncvrlpln2  35281  lplncvrlvol2  35339  dihmeetlem3N  37032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator