Theorem syl6breqr 4928

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

Step	Hyp	Ref	Expression
1		syl6breqr.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		syl6breqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2787	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6breq 4927	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1601   class class class wbr 4886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887

This theorem is referenced by:  pw2eng  8354  cda1en  9332  ackbij1lem9  9385  unsnen  9710  1nqenq  10119  gtndiv  11806  xov1plusxeqvd  12635  intfrac2  12976  serle  13174  discr1  13319  faclbnd4lem1  13398  sqrlem1  14390  sqrlem4  14393  sqrlem7  14396  supcvg  14992  ege2le3  15222  eirrlem  15336  ruclem12  15374  bitsfzo  15563  pcprendvds  15949  pcpremul  15952  pcfaclem  16006  infpnlem2  16019  yonedainv  17307  srgbinomlem4  18930  lmcn2  21861  hmph0  22007  icccmplem2  23034  reconnlem2  23038  xrge0tsms  23045  minveclem2  23632  minveclem3b  23634  minveclem4  23638  minveclem6  23640  ivthlem2  23656  ivthlem3  23657  vitalilem2  23813  itg2seq  23946  itg2monolem1  23954  itg2monolem2  23955  itg2monolem3  23956  dveflem  24179  dvferm1lem  24184  dvferm2lem  24186  c1liplem1  24196  lhop1lem  24213  dvcvx  24220  plyeq0lem  24403  radcnvcl  24608  radcnvle  24611  psercnlem1  24616  psercn  24617  pilem3  24644  pilem3OLD  24645  tangtx  24695  cosne0  24714  recosf1o  24719  resinf1o  24720  efif1olem4  24729  logimul  24797  logcnlem3  24827  logf1o2  24833  ang180lem2  24988  heron  25016  acoscos  25071  emcllem7  25180  fsumharmonic  25190  ftalem2  25252  basellem1  25259  basellem2  25260  basellem3  25261  basellem5  25263  bposlem1  25461  bposlem2  25462  bposlem3  25463  lgsdirprm  25508  chebbnd1lem1  25610  chebbnd1lem2  25611  chebbnd1lem3  25612  mulog2sumlem2  25676  pntpbnd1a  25726  pntpbnd1  25727  pntpbnd2  25728  pntibndlem2  25732  pntlemc  25736  pntlemb  25738  pntlemg  25739  pntlemh  25740  pntlemr  25743  ostth2lem2  25775  ostth2lem3  25776  ostth2lem4  25777  ostth3  25779  axsegconlem3  26268  clwlkclwwlk2  27384  clwlkclwwlk2OLD  27385  siilem1  28278  minvecolem2  28303  minvecolem4  28308  minvecolem5  28309  minvecolem6  28310  nmopcoi  29526  staddi  29677  hgt750lemd  31328  climlec3  32213  logi  32214  poimirlem26  34063  ftc1anclem8  34119  cntotbnd  34221  dalemply  35810  dalemsly  35811  dalem5  35823  dalem13  35832  dalem17  35836  dalem55  35883  dalem57  35885  lhpat3  36202  cdleme22aa  36495  jm2.27c  38537  hashnzfz2  39480  supxrubd  40230  suprnmpt  40283  fzisoeu  40427  upbdrech  40432  recnnltrp  40505  uzublem  40567  fmul01  40724  limsupubuzlem  40856  limsupequzmptlem  40872  ioodvbdlimc1lem2  41079  ioodvbdlimc2lem  41081  stoweidlem36  41184  stoweidlem41  41189  wallispi2  41221  dirkercncflem1  41251  fourierdlem6  41261  fourierdlem7  41262  fourierdlem19  41274  fourierdlem20  41275  fourierdlem24  41279  fourierdlem25  41280  fourierdlem26  41281  fourierdlem30  41285  fourierdlem31  41286  fourierdlem42  41297  fourierdlem47  41301  fourierdlem48  41302  fourierdlem63  41317  fourierdlem64  41318  fourierdlem65  41319  fourierdlem71  41325  fourierdlem79  41333  fourierdlem89  41343  fourierdlem90  41344  fourierdlem91  41345  fouriersw  41379  etransclem28  41410  etransclem48  41430  hoidmv1lelem1  41736  hoidmv1lelem3  41738  hoidmvlelem1  41740  hoidmvlelem4  41743  bgoldbtbndlem2  42723  lincresunit3lem2  43288  lincresunit3  43289  resum2sqgt0  43447  amgmwlem  43658