Theorem breqtrrdi 5189

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 2739	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	breqtrdi 5188	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  enpr2d  9051  enpr2dOLD  9052  pw2eng  9080  undjudom  10164  dju1en  10168  djucomen  10174  djuassen  10175  xpdjuen  10176  infdjuabs  10203  ackbij1lem9  10225  unsnen  10550  1nqenq  10959  gtndiv  12643  xov1plusxeqvd  13479  intfrac2  13827  serle  14027  discr1  14206  faclbnd4lem1  14257  01sqrexlem1  15193  01sqrexlem4  15196  01sqrexlem7  15199  supcvg  15806  ege2le3  16037  eirrlem  16151  ruclem12  16188  bitsfzo  16380  pcprendvds  16777  pcpremul  16780  pcfaclem  16835  infpnlem2  16848  yonedainv  18238  srgbinomlem4  20123  lmcn2  23373  hmph0  23519  icccmplem2  24559  reconnlem2  24563  xrge0tsms  24570  minveclem2  25174  minveclem3b  25176  minveclem4  25180  minveclem6  25182  ivthlem2  25201  ivthlem3  25202  vitalilem2  25358  itg2seq  25492  itg2monolem1  25500  itg2monolem2  25501  itg2monolem3  25502  dveflem  25731  dvferm1lem  25736  dvferm2lem  25738  c1liplem1  25748  lhop1lem  25765  dvcvx  25772  plyeq0lem  25959  radcnvcl  26165  radcnvle  26168  psercnlem1  26173  psercn  26174  pilem3  26201  tangtx  26251  cos02pilt1  26271  cosne0  26274  recosf1o  26280  resinf1o  26281  efif1olem4  26290  logimul  26358  logcnlem3  26388  logf1o2  26394  ang180lem2  26551  heron  26579  acoscos  26634  emcllem7  26742  fsumharmonic  26752  ftalem2  26814  basellem1  26821  basellem2  26822  basellem3  26823  basellem5  26825  bposlem1  27023  bposlem2  27024  bposlem3  27025  lgsdirprm  27070  chebbnd1lem1  27208  chebbnd1lem2  27209  chebbnd1lem3  27210  mulog2sumlem2  27274  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem2  27330  pntlemc  27334  pntlemb  27336  pntlemg  27337  pntlemh  27338  pntlemr  27341  ostth2lem2  27373  ostth2lem3  27374  ostth2lem4  27375  ostth3  27377  axsegconlem3  28444  clwlkclwwlk2  29523  siilem1  30371  minvecolem2  30395  minvecolem4  30400  minvecolem5  30401  minvecolem6  30402  nmopcoi  31615  staddi  31766  cycpmco2lem4  32558  cycpmco2lem5  32559  hgt750lemd  33958  climlec3  35007  logi  35008  poimirlem26  36817  ftc1anclem8  36871  cntotbnd  36967  dalemply  38828  dalemsly  38829  dalem5  38841  dalem13  38850  dalem17  38854  dalem55  38901  dalem57  38903  lhpat3  39220  cdleme22aa  39513  aks4d1p1p7  41245  evlselv  41461  jm2.27c  42048  hashnzfz2  43382  supxrubd  44103  suprnmpt  44171  fzisoeu  44308  upbdrech  44313  recnnltrp  44385  uzublem  44438  fmul01  44594  limsupubuzlem  44726  limsupequzmptlem  44742  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem36  45050  stoweidlem41  45055  wallispi2  45087  dirkercncflem1  45117  fourierdlem6  45127  fourierdlem7  45128  fourierdlem19  45140  fourierdlem20  45141  fourierdlem24  45145  fourierdlem25  45146  fourierdlem26  45147  fourierdlem30  45151  fourierdlem31  45152  fourierdlem42  45163  fourierdlem47  45167  fourierdlem48  45168  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem71  45191  fourierdlem79  45199  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fouriersw  45245  etransclem28  45276  etransclem48  45296  hoidmv1lelem1  45605  hoidmv1lelem3  45607  hoidmvlelem1  45609  hoidmvlelem4  45612  bgoldbtbndlem2  46772  lincresunit3lem2  47248  lincresunit3  47249  resum2sqgt0  47480  amgmwlem  47936