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

Theorem syl6breqr 4402
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 2432 . 2  |-  B  =  C
41, 3syl6breq 4401 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4362
This theorem is referenced by:  pw2eng  7626  cda1en  8551  ackbij1lem9  8604  unsnen  8924  1nqenq  9333  gtndiv  10959  xov1plusxeqvd  11724  intfrac2  12030  serle  12213  discr1  12353  faclbnd4lem1  12423  sqrlem1  13245  sqrlem4  13248  sqrlem7  13251  supcvg  13852  ege2le3  14082  eirrlem  14194  ruclem12  14231  bitsfzo  14347  pcprendvds  14728  pcpremul  14731  pcfaclem  14781  infpnlem2  14793  yonedainv  16104  srgbinomlem4  17714  lmcn2  20601  hmph0  20747  icccmplem2  21778  reconnlem2  21782  xrge0tsms  21789  minveclem2  22305  minveclem3b  22307  minveclem4  22311  minveclem6  22313  minveclem2OLD  22317  minveclem3bOLD  22319  minveclem4OLD  22323  minveclem6OLD  22325  ivthlem2  22340  ivthlem3  22341  vitalilem2  22504  itg2seq  22637  itg2monolem1  22645  itg2monolem2  22646  itg2monolem3  22647  dveflem  22868  dvferm1lem  22873  dvferm2lem  22875  c1liplem1  22885  lhop1lem  22902  dvcvx  22909  plyeq0lem  23101  radcnvcl  23309  radcnvle  23312  psercnlem1  23317  psercn  23318  pilem3  23346  pilem3OLD  23347  tangtx  23397  cosne0  23416  recosf1o  23421  resinf1o  23422  efif1olem4  23431  logimul  23500  logcnlem3  23526  logf1o2  23532  ang180lem2  23676  heron  23701  acoscos  23756  emcllem7  23864  fsumharmonic  23874  ftalem2  23935  basellem1  23944  basellem2  23945  basellem3  23946  basellem5  23948  bposlem1  24149  bposlem2  24150  bposlem3  24151  lgsdirprm  24194  chebbnd1lem1  24244  chebbnd1lem2  24245  chebbnd1lem3  24246  mulog2sumlem2  24310  pntpbnd1a  24360  pntpbnd1  24361  pntpbnd2  24362  pntibndlem2  24366  pntlemc  24370  pntlemb  24372  pntlemg  24373  pntlemh  24374  pntlemr  24377  ostth2lem2  24409  ostth2lem3  24410  ostth2lem4  24411  ostth3  24413  axsegconlem3  24886  clwlkisclwwlk2  25455  eupares  25640  eupap1  25641  siilem1  26429  minvecolem2  26454  minvecolem4  26459  minvecolem5  26460  minvecolem6  26461  minvecolem2OLD  26464  minvecolem4OLD  26469  minvecolem5OLD  26470  minvecolem6OLD  26471  nmopcoi  27685  staddi  27836  climlec3  30315  logi  30316  poimirlem26  31873  ftc1anclem8  31931  cntotbnd  32035  dalemply  33131  dalemsly  33132  dalem5  33144  dalem13  33153  dalem17  33157  dalem55  33204  dalem57  33206  lhpat3  33523  cdleme22aa  33818  jm2.27c  35775  hashnzfz2  36583  suprnmpt  37342  fzisoeu  37415  upbdrech  37420  fmul01  37541  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweidlem36  37780  stoweidlem41  37785  wallispi2  37818  dirkercncflem1  37848  fourierdlem6  37858  fourierdlem7  37859  fourierdlem19  37871  fourierdlem20  37872  fourierdlem24  37876  fourierdlem25  37877  fourierdlem26  37878  fourierdlem30  37882  fourierdlem31  37883  fourierdlem31OLD  37884  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem47  37900  fourierdlem48  37901  fourierdlem63  37916  fourierdlem64  37917  fourierdlem65  37918  fourierdlem71  37924  fourierdlem79  37932  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fouriersw  37978  etransclem28  38010  etransclem48OLD  38030  etransclem48  38031  hoidmv1lelem1  38260  hoidmv1lelem3  38262  hoidmvlelem1  38264  hoidmvlelem4  38267  bgoldbtbndlem2  38714  usgedgleordALT  39323  lincresunit3lem2  39866  lincresunit3  39867
  Copyright terms: Public domain W3C validator