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

Theorem syl6breqr 4435
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 2415 . 2  |-  B  =  C
41, 3syl6breq 4434 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405   class class class wbr 4395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396
This theorem is referenced by:  pw2eng  7661  cda1en  8587  ackbij1lem9  8640  unsnen  8960  1nqenq  9370  gtndiv  10981  xov1plusxeqvd  11720  intfrac2  12023  serle  12206  discr1  12346  faclbnd4lem1  12415  sqrlem1  13225  sqrlem4  13228  sqrlem7  13231  supcvg  13819  ege2le3  14034  eirrlem  14146  ruclem12  14183  bitsfzo  14294  pcprendvds  14573  pcpremul  14576  pcfaclem  14626  infpnlem2  14638  yonedainv  15874  srgbinomlem4  17514  lmcn2  20442  hmph0  20588  icccmplem2  21620  reconnlem2  21624  xrge0tsms  21631  minveclem2  22133  minveclem3b  22135  minveclem4  22139  minveclem6  22141  ivthlem2  22156  ivthlem3  22157  vitalilem2  22310  itg2seq  22441  itg2monolem1  22449  itg2monolem2  22450  itg2monolem3  22451  dveflem  22672  dvferm1lem  22677  dvferm2lem  22679  c1liplem1  22689  lhop1lem  22706  dvcvx  22713  plyeq0lem  22899  radcnvcl  23104  radcnvle  23107  psercnlem1  23112  psercn  23113  pilem3  23140  tangtx  23190  cosne0  23209  recosf1o  23214  resinf1o  23215  efif1olem4  23224  logimul  23293  logcnlem3  23319  logf1o2  23325  ang180lem2  23469  heron  23494  acoscos  23549  emcllem7  23657  fsumharmonic  23667  ftalem2  23728  basellem1  23735  basellem2  23736  basellem3  23737  basellem5  23739  bposlem1  23940  bposlem2  23941  bposlem3  23942  lgsdirprm  23985  chebbnd1lem1  24035  chebbnd1lem2  24036  chebbnd1lem3  24037  mulog2sumlem2  24101  pntpbnd1a  24151  pntpbnd1  24152  pntpbnd2  24153  pntibndlem2  24157  pntlemc  24161  pntlemb  24163  pntlemg  24164  pntlemh  24165  pntlemr  24168  ostth2lem2  24200  ostth2lem3  24201  ostth2lem4  24202  ostth3  24204  axsegconlem3  24639  clwlkisclwwlk2  25207  eupares  25392  eupap1  25393  siilem1  26180  minvecolem2  26205  minvecolem4  26210  minvecolem5  26211  minvecolem6  26212  nmopcoi  27427  staddi  27578  climlec3  29942  logi  29943  ftc1anclem8  31470  cntotbnd  31574  dalemply  32671  dalemsly  32672  dalem5  32684  dalem13  32693  dalem17  32697  dalem55  32744  dalem57  32746  lhpat3  33063  cdleme22aa  33358  jm2.27c  35311  hashnzfz2  36074  suprnmpt  36826  fzisoeu  36869  upbdrech  36874  fmul01  36942  ioodvbdlimc1lem2  37097  ioodvbdlimc2lem  37099  stoweidlem36  37186  stoweidlem41  37191  wallispi2  37223  dirkercncflem1  37253  fourierdlem6  37263  fourierdlem7  37264  fourierdlem19  37276  fourierdlem20  37277  fourierdlem24  37281  fourierdlem25  37282  fourierdlem26  37283  fourierdlem30  37287  fourierdlem31  37288  fourierdlem42  37299  fourierdlem47  37304  fourierdlem48  37305  fourierdlem63  37320  fourierdlem64  37321  fourierdlem65  37322  fourierdlem71  37328  fourierdlem79  37336  fourierdlem89  37346  fourierdlem90  37347  fourierdlem91  37348  fouriersw  37382  etransclem28  37413  etransclem48  37433  bgoldbtbndlem2  37854  usgedgleordALT  38049  lincresunit3lem2  38592  lincresunit3  38593
  Copyright terms: Public domain W3C validator