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

Theorem syl6breqr 4252
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 2440 . 2  |-  B  =  C
41, 3syl6breq 4251 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  pw2eng  7214  cda1en  8055  ackbij1lem9  8108  unsnen  8428  1nqenq  8839  gtndiv  10347  xov1plusxeqvd  11041  intfrac2  11239  serle  11378  discr1  11515  faclbnd4lem1  11584  sqrlem1  12048  sqrlem4  12051  sqrlem7  12054  supcvg  12635  ege2le3  12692  eirrlem  12803  ruclem12  12840  bitsfzo  12947  pcprendvds  13214  pcpremul  13217  pcfaclem  13267  infpnlem2  13279  yonedainv  14378  lmcn2  17681  hmph0  17827  icccmplem2  18854  reconnlem2  18858  xrge0tsms  18865  minveclem2  19327  minveclem3b  19329  minveclem4  19333  minveclem6  19335  ivthlem2  19349  ivthlem3  19350  vitalilem2  19501  itg2seq  19634  itg2monolem1  19642  itg2monolem2  19643  itg2monolem3  19644  dveflem  19863  dvferm1lem  19868  dvferm2lem  19870  c1liplem1  19880  lhop1lem  19897  dvcvx  19904  plyeq0lem  20129  radcnvcl  20333  radcnvle  20336  psercnlem1  20341  psercn  20342  pilem3  20369  tangtx  20413  cosne0  20432  recosf1o  20437  resinf1o  20438  efif1olem4  20447  logimul  20509  logcnlem3  20535  logf1o2  20541  ang180lem2  20652  acoscos  20733  emcllem7  20840  fsumharmonic  20850  ftalem2  20856  basellem1  20863  basellem2  20864  basellem3  20865  basellem5  20867  bposlem1  21068  bposlem2  21069  bposlem3  21070  lgsdirprm  21113  chebbnd1lem1  21163  chebbnd1lem2  21164  chebbnd1lem3  21165  mulog2sumlem2  21229  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntibndlem2  21285  pntlemc  21289  pntlemb  21291  pntlemg  21292  pntlemh  21293  pntlemr  21296  ostth2lem2  21328  ostth2lem3  21329  ostth2lem4  21330  ostth3  21332  eupares  21697  eupap1  21698  siilem1  22352  minvecolem2  22377  minvecolem4  22382  minvecolem5  22383  minvecolem6  22384  nmopcoi  23598  staddi  23749  climlec3  25214  axsegconlem3  25858  ftc1anclem8  26287  cntotbnd  26505  jm2.27c  27078  fmul01  27686  stoweidlem36  27761  stoweidlem41  27766  wallispi2  27798  lstccats1fst  28263  dalemply  30451  dalemsly  30452  dalem5  30464  dalem13  30473  dalem17  30477  dalem55  30524  dalem57  30526  lhpat3  30843  cdleme22aa  31136
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator