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

Theorem syl6breqr 4625
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 2619 . 2 𝐵 = 𝐶
41, 3syl6breq 4624 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584
This theorem is referenced by:  pw2eng  7951  cda1en  8880  ackbij1lem9  8933  unsnen  9254  1nqenq  9663  gtndiv  11330  xov1plusxeqvd  12189  intfrac2  12519  serle  12718  discr1  12862  faclbnd4lem1  12942  sqrlem1  13831  sqrlem4  13834  sqrlem7  13837  supcvg  14427  ege2le3  14659  eirrlem  14771  ruclem12  14809  bitsfzo  14995  pcprendvds  15383  pcpremul  15386  pcfaclem  15440  infpnlem2  15453  yonedainv  16744  srgbinomlem4  18366  lmcn2  21262  hmph0  21408  icccmplem2  22434  reconnlem2  22438  xrge0tsms  22445  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  ivthlem2  23028  ivthlem3  23029  vitalilem2  23184  itg2seq  23315  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  c1liplem1  23563  lhop1lem  23580  dvcvx  23587  plyeq0lem  23770  radcnvcl  23975  radcnvle  23978  psercnlem1  23983  psercn  23984  pilem3  24011  tangtx  24061  cosne0  24080  recosf1o  24085  resinf1o  24086  efif1olem4  24095  logimul  24164  logcnlem3  24190  logf1o2  24196  ang180lem2  24340  heron  24365  acoscos  24420  emcllem7  24528  fsumharmonic  24538  ftalem2  24600  basellem1  24607  basellem2  24608  basellem3  24609  basellem5  24611  bposlem1  24809  bposlem2  24810  bposlem3  24811  lgsdirprm  24856  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  mulog2sumlem2  25024  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemc  25084  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemr  25091  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth3  25127  axsegconlem3  25599  clwlkisclwwlk2  26318  eupares  26502  eupap1  26503  siilem1  27090  minvecolem2  27115  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  nmopcoi  28338  staddi  28489  climlec3  30872  logi  30873  poimirlem26  32605  ftc1anclem8  32662  cntotbnd  32765  dalemply  33958  dalemsly  33959  dalem5  33971  dalem13  33980  dalem17  33984  dalem55  34031  dalem57  34033  lhpat3  34350  cdleme22aa  34645  jm2.27c  36592  hashnzfz2  37542  supxrubd  38328  suprnmpt  38350  fzisoeu  38455  upbdrech  38460  recnnltrp  38534  fmul01  38647  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem36  38929  stoweidlem41  38934  wallispi2  38966  dirkercncflem1  38996  fourierdlem6  39006  fourierdlem7  39007  fourierdlem19  39019  fourierdlem20  39020  fourierdlem24  39024  fourierdlem25  39025  fourierdlem26  39026  fourierdlem30  39030  fourierdlem31  39031  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem71  39070  fourierdlem79  39078  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fouriersw  39124  etransclem28  39155  etransclem48  39175  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmvlelem1  39485  hoidmvlelem4  39488  bgoldbtbndlem2  40222  clwlkclwwlk2  41212  lincresunit3lem2  42063  lincresunit3  42064  amgmwlem  42357
  Copyright terms: Public domain W3C validator