Theorem breqtrrdi 5141

Description: A chained equality inference for a binary relation. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
breqtrrdi.1	⊢ (𝜑 → 𝐴𝑅𝐵)
breqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
breqtrrdi	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem breqtrrdi

Step	Hyp	Ref	Expression
1		breqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		breqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2746	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5140	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  enpr2d  8989  pw2eng  9015  undjudom  10082  dju1en  10086  djucomen  10092  djuassen  10093  xpdjuen  10094  infdjuabs  10119  ackbij1lem9  10141  unsnen  10467  1nqenq  10877  gtndiv  12573  xov1plusxeqvd  13418  intfrac2  13782  serle  13984  discr1  14166  faclbnd4lem1  14220  01sqrexlem1  15169  01sqrexlem4  15172  01sqrexlem7  15175  supcvg  15783  ege2le3  16017  eirrlem  16133  ruclem12  16170  bitsfzo  16366  pcprendvds  16772  pcpremul  16775  pcfaclem  16830  infpnlem2  16843  yonedainv  18208  srgbinomlem4  20168  lmcn2  23597  hmph0  23743  icccmplem2  24772  reconnlem2  24776  xrge0tsms  24783  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  ivthlem2  25413  ivthlem3  25414  vitalilem2  25570  itg2seq  25703  itg2monolem1  25711  itg2monolem2  25712  itg2monolem3  25713  dveflem  25943  dvferm1lem  25948  dvferm2lem  25950  c1liplem1  25961  lhop1lem  25978  dvcvx  25985  plyeq0lem  26175  radcnvcl  26386  radcnvle  26389  psercnlem1  26395  psercn  26396  pilem3  26423  tangtx  26474  cos02pilt1  26495  cosne0  26498  recosf1o  26504  resinf1o  26505  efif1olem4  26514  logi  26556  logimul  26583  logcnlem3  26613  logf1o2  26619  ang180lem2  26780  heron  26808  acoscos  26863  emcllem7  26972  fsumharmonic  26982  ftalem2  27044  basellem1  27051  basellem2  27052  basellem3  27053  basellem5  27055  bposlem1  27255  bposlem2  27256  bposlem3  27257  lgsdirprm  27302  chebbnd1lem1  27440  chebbnd1lem2  27441  chebbnd1lem3  27442  mulog2sumlem2  27506  pntpbnd1a  27556  pntpbnd1  27557  pntpbnd2  27558  pntibndlem2  27562  pntlemc  27566  pntlemb  27568  pntlemg  27569  pntlemh  27570  pntlemr  27573  ostth2lem2  27605  ostth2lem3  27606  ostth2lem4  27607  ostth3  27609  axsegconlem3  28996  clwlkclwwlk2  30082  siilem1  30930  minvecolem2  30954  minvecolem4  30959  minvecolem5  30960  minvecolem6  30961  nmopcoi  32174  staddi  32325  cycpmco2lem4  33213  cycpmco2lem5  33214  iconstr  33925  hgt750lemd  34807  climlec3  35930  poimirlem26  37849  ftc1anclem8  37903  cntotbnd  37999  dalemply  39982  dalemsly  39983  dalem5  39995  dalem13  40004  dalem17  40008  dalem55  40055  dalem57  40057  lhpat3  40374  cdleme22aa  40667  aks4d1p1p7  42396  evlselv  42897  jm2.27c  43316  hashnzfz2  44629  supxrubd  45424  suprnmpt  45485  fzisoeu  45615  upbdrech  45620  recnnltrp  45688  uzublem  45741  fmul01  45893  limsupubuzlem  46023  limsupequzmptlem  46039  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweidlem36  46347  stoweidlem41  46352  wallispi2  46384  dirkercncflem1  46414  fourierdlem6  46424  fourierdlem7  46425  fourierdlem19  46437  fourierdlem20  46438  fourierdlem24  46442  fourierdlem25  46443  fourierdlem26  46444  fourierdlem30  46448  fourierdlem31  46449  fourierdlem42  46460  fourierdlem47  46464  fourierdlem48  46465  fourierdlem63  46480  fourierdlem64  46481  fourierdlem65  46482  fourierdlem71  46488  fourierdlem79  46496  fourierdlem89  46506  fourierdlem90  46507  fourierdlem91  46508  fouriersw  46542  etransclem28  46573  etransclem48  46593  hoidmv1lelem1  46902  hoidmv1lelem3  46904  hoidmvlelem1  46906  hoidmvlelem4  46909  bgoldbtbndlem2  48119  gpg3kgrtriexlem4  48399  gpg3kgrtriexlem6  48401  lincresunit3lem2  48793  lincresunit3  48794  resum2sqgt0  49020  amgmwlem  50114