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

Theorem syl6breqr 4439
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 2467 . 2  |-  B  =  C
41, 3syl6breq 4438 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   class class class wbr 4399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400
This theorem is referenced by:  pw2eng  7526  cda1en  8454  ackbij1lem9  8507  unsnen  8827  1nqenq  9241  gtndiv  10829  xov1plusxeqvd  11547  intfrac2  11813  serle  11977  discr1  12116  faclbnd4lem1  12185  sqrlem1  12849  sqrlem4  12852  sqrlem7  12855  supcvg  13435  ege2le3  13492  eirrlem  13603  ruclem12  13640  bitsfzo  13748  pcprendvds  14024  pcpremul  14027  pcfaclem  14077  infpnlem2  14089  yonedainv  15209  srgbinomlem4  16763  lmcn2  19353  hmph0  19499  icccmplem2  20531  reconnlem2  20535  xrge0tsms  20542  minveclem2  21044  minveclem3b  21046  minveclem4  21050  minveclem6  21052  ivthlem2  21067  ivthlem3  21068  vitalilem2  21221  itg2seq  21352  itg2monolem1  21360  itg2monolem2  21361  itg2monolem3  21362  dveflem  21583  dvferm1lem  21588  dvferm2lem  21590  c1liplem1  21600  lhop1lem  21617  dvcvx  21624  plyeq0lem  21810  radcnvcl  22014  radcnvle  22017  psercnlem1  22022  psercn  22023  pilem3  22050  tangtx  22099  cosne0  22118  recosf1o  22123  resinf1o  22124  efif1olem4  22133  logimul  22195  logcnlem3  22221  logf1o2  22227  ang180lem2  22338  heron  22365  acoscos  22420  emcllem7  22527  fsumharmonic  22537  ftalem2  22543  basellem1  22550  basellem2  22551  basellem3  22552  basellem5  22554  bposlem1  22755  bposlem2  22756  bposlem3  22757  lgsdirprm  22800  chebbnd1lem1  22850  chebbnd1lem2  22851  chebbnd1lem3  22852  mulog2sumlem2  22916  pntpbnd1a  22966  pntpbnd1  22967  pntpbnd2  22968  pntibndlem2  22972  pntlemc  22976  pntlemb  22978  pntlemg  22979  pntlemh  22980  pntlemr  22983  ostth2lem2  23015  ostth2lem3  23016  ostth2lem4  23017  ostth3  23019  axsegconlem3  23316  eupares  23747  eupap1  23748  siilem1  24402  minvecolem2  24427  minvecolem4  24432  minvecolem5  24433  minvecolem6  24434  nmopcoi  25650  staddi  25801  climlec3  27544  ftc1anclem8  28621  cntotbnd  28842  jm2.27c  29503  fmul01  29908  stoweidlem36  29978  stoweidlem41  29983  wallispi2  30015  clwlkisclwwlk2  30599  lincresunit3lem2  31132  lincresunit3  31133  dalemply  33621  dalemsly  33622  dalem5  33634  dalem13  33643  dalem17  33647  dalem55  33694  dalem57  33696  lhpat3  34013  cdleme22aa  34306
  Copyright terms: Public domain W3C validator