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

Theorem syl6breqr 4473
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 2454 . 2  |-  B  =  C
41, 3syl6breq 4472 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381   class class class wbr 4433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434
This theorem is referenced by:  pw2eng  7621  cda1en  8553  ackbij1lem9  8606  unsnen  8926  1nqenq  9338  gtndiv  10941  xov1plusxeqvd  11670  intfrac2  11959  serle  12136  discr1  12276  faclbnd4lem1  12345  sqrlem1  13050  sqrlem4  13053  sqrlem7  13056  supcvg  13641  ege2le3  13698  eirrlem  13809  ruclem12  13846  bitsfzo  13957  pcprendvds  14236  pcpremul  14239  pcfaclem  14289  infpnlem2  14301  yonedainv  15419  srgbinomlem4  17062  lmcn2  20016  hmph0  20162  icccmplem2  21194  reconnlem2  21198  xrge0tsms  21205  minveclem2  21707  minveclem3b  21709  minveclem4  21713  minveclem6  21715  ivthlem2  21730  ivthlem3  21731  vitalilem2  21884  itg2seq  22015  itg2monolem1  22023  itg2monolem2  22024  itg2monolem3  22025  dveflem  22246  dvferm1lem  22251  dvferm2lem  22253  c1liplem1  22263  lhop1lem  22280  dvcvx  22287  plyeq0lem  22473  radcnvcl  22677  radcnvle  22680  psercnlem1  22685  psercn  22686  pilem3  22713  tangtx  22763  cosne0  22782  recosf1o  22787  resinf1o  22788  efif1olem4  22797  logimul  22864  logcnlem3  22890  logf1o2  22896  ang180lem2  23007  heron  23034  acoscos  23089  emcllem7  23196  fsumharmonic  23206  ftalem2  23212  basellem1  23219  basellem2  23220  basellem3  23221  basellem5  23223  bposlem1  23424  bposlem2  23425  bposlem3  23426  lgsdirprm  23469  chebbnd1lem1  23519  chebbnd1lem2  23520  chebbnd1lem3  23521  mulog2sumlem2  23585  pntpbnd1a  23635  pntpbnd1  23636  pntpbnd2  23637  pntibndlem2  23641  pntlemc  23645  pntlemb  23647  pntlemg  23648  pntlemh  23649  pntlemr  23652  ostth2lem2  23684  ostth2lem3  23685  ostth2lem4  23686  ostth3  23688  axsegconlem3  24087  clwlkisclwwlk2  24655  eupares  24840  eupap1  24841  siilem1  25631  minvecolem2  25656  minvecolem4  25661  minvecolem5  25662  minvecolem6  25663  nmopcoi  26879  staddi  27030  climlec3  28988  ftc1anclem8  30065  cntotbnd  30260  jm2.27c  30917  hashnzfz2  31195  suprnmpt  31397  fzisoeu  31445  upbdrech  31450  fmul01  31498  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  stoweidlem36  31703  stoweidlem41  31708  wallispi2  31740  dirkercncflem1  31770  fourierdlem6  31780  fourierdlem7  31781  fourierdlem19  31793  fourierdlem20  31794  fourierdlem24  31798  fourierdlem25  31799  fourierdlem26  31800  fourierdlem30  31804  fourierdlem31  31805  fourierdlem42  31816  fourierdlem47  31821  fourierdlem48  31822  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem71  31845  fourierdlem79  31853  fourierdlem89  31863  fourierdlem90  31864  fourierdlem91  31865  fouriersw  31899  usgedgleordALT  32254  lincresunit3lem2  32791  lincresunit3  32792  dalemply  35080  dalemsly  35081  dalem5  35093  dalem13  35102  dalem17  35106  dalem55  35153  dalem57  35155  lhpat3  35472  cdleme22aa  35767
  Copyright terms: Public domain W3C validator