Theorem breqtrrdi 5191

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  enpr2d  9049  enpr2dOLD  9050  pw2eng  9078  undjudom  10162  dju1en  10166  djucomen  10172  djuassen  10173  xpdjuen  10174  infdjuabs  10201  ackbij1lem9  10223  unsnen  10548  1nqenq  10957  gtndiv  12639  xov1plusxeqvd  13475  intfrac2  13823  serle  14023  discr1  14202  faclbnd4lem1  14253  01sqrexlem1  15189  01sqrexlem4  15192  01sqrexlem7  15195  supcvg  15802  ege2le3  16033  eirrlem  16147  ruclem12  16184  bitsfzo  16376  pcprendvds  16773  pcpremul  16776  pcfaclem  16831  infpnlem2  16844  yonedainv  18234  srgbinomlem4  20052  lmcn2  23153  hmph0  23299  icccmplem2  24339  reconnlem2  24343  xrge0tsms  24350  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  ivthlem2  24969  ivthlem3  24970  vitalilem2  25126  itg2seq  25260  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  dveflem  25496  dvferm1lem  25501  dvferm2lem  25503  c1liplem1  25513  lhop1lem  25530  dvcvx  25537  plyeq0lem  25724  radcnvcl  25929  radcnvle  25932  psercnlem1  25937  psercn  25938  pilem3  25965  tangtx  26015  cos02pilt1  26035  cosne0  26038  recosf1o  26044  resinf1o  26045  efif1olem4  26054  logimul  26122  logcnlem3  26152  logf1o2  26158  ang180lem2  26315  heron  26343  acoscos  26398  emcllem7  26506  fsumharmonic  26516  ftalem2  26578  basellem1  26585  basellem2  26586  basellem3  26587  basellem5  26589  bposlem1  26787  bposlem2  26788  bposlem3  26789  lgsdirprm  26834  chebbnd1lem1  26972  chebbnd1lem2  26973  chebbnd1lem3  26974  mulog2sumlem2  27038  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntibndlem2  27094  pntlemc  27098  pntlemb  27100  pntlemg  27101  pntlemh  27102  pntlemr  27105  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  ostth3  27141  axsegconlem3  28177  clwlkclwwlk2  29256  siilem1  30104  minvecolem2  30128  minvecolem4  30133  minvecolem5  30134  minvecolem6  30135  nmopcoi  31348  staddi  31499  cycpmco2lem4  32288  cycpmco2lem5  32289  hgt750lemd  33660  climlec3  34703  logi  34704  poimirlem26  36514  ftc1anclem8  36568  cntotbnd  36664  dalemply  38525  dalemsly  38526  dalem5  38538  dalem13  38547  dalem17  38551  dalem55  38598  dalem57  38600  lhpat3  38917  cdleme22aa  39210  aks4d1p1p7  40939  evlselv  41159  jm2.27c  41746  hashnzfz2  43080  supxrubd  43802  suprnmpt  43870  fzisoeu  44010  upbdrech  44015  recnnltrp  44087  uzublem  44140  fmul01  44296  limsupubuzlem  44428  limsupequzmptlem  44444  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem36  44752  stoweidlem41  44757  wallispi2  44789  dirkercncflem1  44819  fourierdlem6  44829  fourierdlem7  44830  fourierdlem19  44842  fourierdlem20  44843  fourierdlem24  44847  fourierdlem25  44848  fourierdlem26  44849  fourierdlem30  44853  fourierdlem31  44854  fourierdlem42  44865  fourierdlem47  44869  fourierdlem48  44870  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem71  44893  fourierdlem79  44901  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fouriersw  44947  etransclem28  44978  etransclem48  44998  hoidmv1lelem1  45307  hoidmv1lelem3  45309  hoidmvlelem1  45311  hoidmvlelem4  45314  bgoldbtbndlem2  46474  lincresunit3lem2  47161  lincresunit3  47162  resum2sqgt0  47393  amgmwlem  47849