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

Theorem syl6breqr 4457
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6breqr.1  |-  ( ph  ->  A R B )
syl6breqr.2  |-  C  =  B
Assertion
Ref Expression
syl6breqr  |-  ( ph  ->  A R C )

Proof of Theorem syl6breqr
StepHypRef Expression
1 syl6breqr.1 . 2  |-  ( ph  ->  A R B )
2 syl6breqr.2 . . 3  |-  C  =  B
32eqcomi 2471 . 2  |-  B  =  C
41, 3syl6breq 4456 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   class class class wbr 4416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417
This theorem is referenced by:  pw2eng  7704  cda1en  8631  ackbij1lem9  8684  unsnen  9004  1nqenq  9413  gtndiv  11042  xov1plusxeqvd  11807  intfrac2  12117  serle  12300  discr1  12440  faclbnd4lem1  12510  sqrlem1  13355  sqrlem4  13358  sqrlem7  13361  supcvg  13963  ege2le3  14193  eirrlem  14305  ruclem12  14342  bitsfzo  14458  pcprendvds  14839  pcpremul  14842  pcfaclem  14892  infpnlem2  14904  yonedainv  16215  srgbinomlem4  17825  lmcn2  20713  hmph0  20859  icccmplem2  21890  reconnlem2  21894  xrge0tsms  21901  minveclem2  22417  minveclem3b  22419  minveclem4  22423  minveclem6  22425  minveclem2OLD  22429  minveclem3bOLD  22431  minveclem4OLD  22435  minveclem6OLD  22437  ivthlem2  22452  ivthlem3  22453  vitalilem2  22616  itg2seq  22749  itg2monolem1  22757  itg2monolem2  22758  itg2monolem3  22759  dveflem  22980  dvferm1lem  22985  dvferm2lem  22987  c1liplem1  22997  lhop1lem  23014  dvcvx  23021  plyeq0lem  23213  radcnvcl  23421  radcnvle  23424  psercnlem1  23429  psercn  23430  pilem3  23458  pilem3OLD  23459  tangtx  23509  cosne0  23528  recosf1o  23533  resinf1o  23534  efif1olem4  23543  logimul  23612  logcnlem3  23638  logf1o2  23644  ang180lem2  23788  heron  23813  acoscos  23868  emcllem7  23976  fsumharmonic  23986  ftalem2  24047  basellem1  24056  basellem2  24057  basellem3  24058  basellem5  24060  bposlem1  24261  bposlem2  24262  bposlem3  24263  lgsdirprm  24306  chebbnd1lem1  24356  chebbnd1lem2  24357  chebbnd1lem3  24358  mulog2sumlem2  24422  pntpbnd1a  24472  pntpbnd1  24473  pntpbnd2  24474  pntibndlem2  24478  pntlemc  24482  pntlemb  24484  pntlemg  24485  pntlemh  24486  pntlemr  24489  ostth2lem2  24521  ostth2lem3  24522  ostth2lem4  24523  ostth3  24525  axsegconlem3  24998  clwlkisclwwlk2  25567  eupares  25752  eupap1  25753  siilem1  26541  minvecolem2  26566  minvecolem4  26571  minvecolem5  26572  minvecolem6  26573  minvecolem2OLD  26576  minvecolem4OLD  26581  minvecolem5OLD  26582  minvecolem6OLD  26583  nmopcoi  27797  staddi  27948  climlec3  30418  logi  30419  poimirlem26  32011  ftc1anclem8  32069  cntotbnd  32173  dalemply  33264  dalemsly  33265  dalem5  33277  dalem13  33286  dalem17  33290  dalem55  33337  dalem57  33339  lhpat3  33656  cdleme22aa  33951  jm2.27c  35907  hashnzfz2  36714  suprnmpt  37477  fzisoeu  37556  upbdrech  37561  fmul01  37696  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  stoweidlem36  37935  stoweidlem41  37940  wallispi2  37973  dirkercncflem1  38003  fourierdlem6  38013  fourierdlem7  38014  fourierdlem19  38026  fourierdlem20  38027  fourierdlem24  38031  fourierdlem25  38032  fourierdlem26  38033  fourierdlem30  38037  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem47  38055  fourierdlem48  38056  fourierdlem63  38071  fourierdlem64  38072  fourierdlem65  38073  fourierdlem71  38079  fourierdlem79  38087  fourierdlem89  38097  fourierdlem90  38098  fourierdlem91  38099  fouriersw  38133  etransclem28  38165  etransclem48OLD  38185  etransclem48  38186  hoidmv1lelem1  38451  hoidmv1lelem3  38453  hoidmvlelem1  38455  hoidmvlelem4  38458  bgoldbtbndlem2  38939  usgedgleordALT  40005  lincresunit3lem2  40546  lincresunit3  40547
  Copyright terms: Public domain W3C validator