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

Theorem syl6breqr 4839
Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6breqr.1 (𝜑𝐴𝑅𝐵)
syl6breqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6breqr (𝜑𝐴𝑅𝐶)

Proof of Theorem syl6breqr
StepHypRef Expression
1 syl6breqr.1 . 2 (𝜑𝐴𝑅𝐵)
2 syl6breqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2783 . 2 𝐵 = 𝐶
41, 3syl6breq 4838 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1634   class class class wbr 4797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798
This theorem is referenced by:  pw2eng  8243  cda1en  9220  ackbij1lem9  9273  unsnen  9598  1nqenq  10007  gtndiv  11678  xov1plusxeqvd  12547  intfrac2  12887  serle  13085  discr1  13229  faclbnd4lem1  13306  sqrlem1  14213  sqrlem4  14216  sqrlem7  14219  supcvg  14817  ege2le3  15048  eirrlem  15160  ruclem12  15198  bitsfzo  15386  pcprendvds  15772  pcpremul  15775  pcfaclem  15829  infpnlem2  15842  yonedainv  17149  srgbinomlem4  18771  lmcn2  21693  hmph0  21839  icccmplem2  22866  reconnlem2  22870  xrge0tsms  22877  minveclem2  23436  minveclem3b  23438  minveclem4  23442  minveclem6  23444  ivthlem2  23460  ivthlem3  23461  vitalilem2  23617  itg2seq  23750  itg2monolem1  23758  itg2monolem2  23759  itg2monolem3  23760  dveflem  23983  dvferm1lem  23988  dvferm2lem  23990  c1liplem1  24000  lhop1lem  24017  dvcvx  24024  plyeq0lem  24207  radcnvcl  24412  radcnvle  24415  psercnlem1  24420  psercn  24421  pilem3  24448  pilem3OLD  24449  tangtx  24499  cosne0  24518  recosf1o  24523  resinf1o  24524  efif1olem4  24533  logimul  24602  logcnlem3  24632  logf1o2  24638  ang180lem2  24782  heron  24807  acoscos  24862  emcllem7  24970  fsumharmonic  24980  ftalem2  25042  basellem1  25049  basellem2  25050  basellem3  25051  basellem5  25053  bposlem1  25251  bposlem2  25252  bposlem3  25253  lgsdirprm  25298  chebbnd1lem1  25400  chebbnd1lem2  25401  chebbnd1lem3  25402  mulog2sumlem2  25466  pntpbnd1a  25516  pntpbnd1  25517  pntpbnd2  25518  pntibndlem2  25522  pntlemc  25526  pntlemb  25528  pntlemg  25529  pntlemh  25530  pntlemr  25533  ostth2lem2  25565  ostth2lem3  25566  ostth2lem4  25567  ostth3  25569  axsegconlem3  26041  clwlkclwwlk2  27174  siilem1  28063  minvecolem2  28088  minvecolem4  28093  minvecolem5  28094  minvecolem6  28095  nmopcoi  29311  staddi  29462  hgt750lemd  31083  climlec3  31974  logi  31975  poimirlem26  33785  ftc1anclem8  33841  cntotbnd  33943  dalemply  35478  dalemsly  35479  dalem5  35491  dalem13  35500  dalem17  35504  dalem55  35551  dalem57  35553  lhpat3  35870  cdleme22aa  36164  jm2.27c  38115  hashnzfz2  39060  supxrubd  39830  suprnmpt  39886  fzisoeu  40039  upbdrech  40044  recnnltrp  40117  uzublem  40180  fmul01  40336  limsupubuzlem  40468  limsupequzmptlem  40484  ioodvbdlimc1lem2  40671  ioodvbdlimc2lem  40673  stoweidlem36  40776  stoweidlem41  40781  wallispi2  40813  dirkercncflem1  40843  fourierdlem6  40853  fourierdlem7  40854  fourierdlem19  40866  fourierdlem20  40867  fourierdlem24  40871  fourierdlem25  40872  fourierdlem26  40873  fourierdlem30  40877  fourierdlem31  40878  fourierdlem42  40889  fourierdlem47  40893  fourierdlem48  40894  fourierdlem63  40909  fourierdlem64  40910  fourierdlem65  40911  fourierdlem71  40917  fourierdlem79  40925  fourierdlem89  40935  fourierdlem90  40936  fourierdlem91  40937  fouriersw  40971  etransclem28  41002  etransclem48  41022  hoidmv1lelem1  41331  hoidmv1lelem3  41333  hoidmvlelem1  41335  hoidmvlelem4  41338  bgoldbtbndlem2  42246  lincresunit3lem2  42821  lincresunit3  42822  amgmwlem  43103
  Copyright terms: Public domain W3C validator