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

Theorem syl6breqr 4686
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 2629 . 2 𝐵 = 𝐶
41, 3syl6breq 4685 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481   class class class wbr 4644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645
This theorem is referenced by:  pw2eng  8051  cda1en  8982  ackbij1lem9  9035  unsnen  9360  1nqenq  9769  gtndiv  11439  xov1plusxeqvd  12303  intfrac2  12640  serle  12839  discr1  12983  faclbnd4lem1  13063  sqrlem1  13964  sqrlem4  13967  sqrlem7  13970  supcvg  14569  ege2le3  14801  eirrlem  14913  ruclem12  14951  bitsfzo  15138  pcprendvds  15526  pcpremul  15529  pcfaclem  15583  infpnlem2  15596  yonedainv  16902  srgbinomlem4  18524  lmcn2  21433  hmph0  21579  icccmplem2  22607  reconnlem2  22611  xrge0tsms  22618  minveclem2  23178  minveclem3b  23180  minveclem4  23184  minveclem6  23186  ivthlem2  23202  ivthlem3  23203  vitalilem2  23359  itg2seq  23490  itg2monolem1  23498  itg2monolem2  23499  itg2monolem3  23500  dveflem  23723  dvferm1lem  23728  dvferm2lem  23730  c1liplem1  23740  lhop1lem  23757  dvcvx  23764  plyeq0lem  23947  radcnvcl  24152  radcnvle  24155  psercnlem1  24160  psercn  24161  pilem3  24188  tangtx  24238  cosne0  24257  recosf1o  24262  resinf1o  24263  efif1olem4  24272  logimul  24341  logcnlem3  24371  logf1o2  24377  ang180lem2  24521  heron  24546  acoscos  24601  emcllem7  24709  fsumharmonic  24719  ftalem2  24781  basellem1  24788  basellem2  24789  basellem3  24790  basellem5  24792  bposlem1  24990  bposlem2  24991  bposlem3  24992  lgsdirprm  25037  chebbnd1lem1  25139  chebbnd1lem2  25140  chebbnd1lem3  25141  mulog2sumlem2  25205  pntpbnd1a  25255  pntpbnd1  25256  pntpbnd2  25257  pntibndlem2  25261  pntlemc  25265  pntlemb  25267  pntlemg  25268  pntlemh  25269  pntlemr  25272  ostth2lem2  25304  ostth2lem3  25305  ostth2lem4  25306  ostth3  25308  axsegconlem3  25780  clwlkclwwlk2  26885  siilem1  27676  minvecolem2  27701  minvecolem4  27706  minvecolem5  27707  minvecolem6  27708  nmopcoi  28924  staddi  29075  hgt750lemd  30700  climlec3  31594  logi  31595  poimirlem26  33406  ftc1anclem8  33463  cntotbnd  33566  dalemply  34759  dalemsly  34760  dalem5  34772  dalem13  34781  dalem17  34785  dalem55  34832  dalem57  34834  lhpat3  35151  cdleme22aa  35446  jm2.27c  37393  hashnzfz2  38340  supxrubd  39117  suprnmpt  39171  fzisoeu  39327  upbdrech  39332  recnnltrp  39406  uzublem  39470  fmul01  39612  limsupubuzlem  39744  limsupequzmptlem  39760  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  stoweidlem36  40016  stoweidlem41  40021  wallispi2  40053  dirkercncflem1  40083  fourierdlem6  40093  fourierdlem7  40094  fourierdlem19  40106  fourierdlem20  40107  fourierdlem24  40111  fourierdlem25  40112  fourierdlem26  40113  fourierdlem30  40117  fourierdlem31  40118  fourierdlem42  40129  fourierdlem47  40133  fourierdlem48  40134  fourierdlem63  40149  fourierdlem64  40150  fourierdlem65  40151  fourierdlem71  40157  fourierdlem79  40165  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fouriersw  40211  etransclem28  40242  etransclem48  40262  hoidmv1lelem1  40568  hoidmv1lelem3  40570  hoidmvlelem1  40572  hoidmvlelem4  40575  bgoldbtbndlem2  41459  lincresunit3lem2  42034  lincresunit3  42035  amgmwlem  42313
  Copyright terms: Public domain W3C validator