Theorem breqtrrdi 5149

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  enpr2d  9020  enpr2dOLD  9021  pw2eng  9047  undjudom  10121  dju1en  10125  djucomen  10131  djuassen  10132  xpdjuen  10133  infdjuabs  10158  ackbij1lem9  10180  unsnen  10506  1nqenq  10915  gtndiv  12611  xov1plusxeqvd  13459  intfrac2  13820  serle  14022  discr1  14204  faclbnd4lem1  14258  01sqrexlem1  15208  01sqrexlem4  15211  01sqrexlem7  15214  supcvg  15822  ege2le3  16056  eirrlem  16172  ruclem12  16209  bitsfzo  16405  pcprendvds  16811  pcpremul  16814  pcfaclem  16869  infpnlem2  16882  yonedainv  18242  srgbinomlem4  20138  lmcn2  23536  hmph0  23682  icccmplem2  24712  reconnlem2  24716  xrge0tsms  24723  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  ivthlem2  25353  ivthlem3  25354  vitalilem2  25510  itg2seq  25643  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  dveflem  25883  dvferm1lem  25888  dvferm2lem  25890  c1liplem1  25901  lhop1lem  25918  dvcvx  25925  plyeq0lem  26115  radcnvcl  26326  radcnvle  26329  psercnlem1  26335  psercn  26336  pilem3  26363  tangtx  26414  cos02pilt1  26435  cosne0  26438  recosf1o  26444  resinf1o  26445  efif1olem4  26454  logi  26496  logimul  26523  logcnlem3  26553  logf1o2  26559  ang180lem2  26720  heron  26748  acoscos  26803  emcllem7  26912  fsumharmonic  26922  ftalem2  26984  basellem1  26991  basellem2  26992  basellem3  26993  basellem5  26995  bposlem1  27195  bposlem2  27196  bposlem3  27197  lgsdirprm  27242  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  mulog2sumlem2  27446  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntlemc  27506  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemr  27513  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth3  27549  axsegconlem3  28846  clwlkclwwlk2  29932  siilem1  30780  minvecolem2  30804  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  nmopcoi  32024  staddi  32175  cycpmco2lem4  33086  cycpmco2lem5  33087  iconstr  33756  hgt750lemd  34639  climlec3  35721  poimirlem26  37640  ftc1anclem8  37694  cntotbnd  37790  dalemply  39648  dalemsly  39649  dalem5  39661  dalem13  39670  dalem17  39674  dalem55  39721  dalem57  39723  lhpat3  40040  cdleme22aa  40333  aks4d1p1p7  42062  evlselv  42575  jm2.27c  42996  hashnzfz2  44310  supxrubd  45107  suprnmpt  45168  fzisoeu  45298  upbdrech  45303  recnnltrp  45373  uzublem  45426  fmul01  45578  limsupubuzlem  45710  limsupequzmptlem  45726  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem36  46034  stoweidlem41  46039  wallispi2  46071  dirkercncflem1  46101  fourierdlem6  46111  fourierdlem7  46112  fourierdlem19  46124  fourierdlem20  46125  fourierdlem24  46129  fourierdlem25  46130  fourierdlem26  46131  fourierdlem30  46135  fourierdlem31  46136  fourierdlem42  46147  fourierdlem47  46151  fourierdlem48  46152  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem71  46175  fourierdlem79  46183  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fouriersw  46229  etransclem28  46260  etransclem48  46280  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem4  46596  bgoldbtbndlem2  47807  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  lincresunit3lem2  48469  lincresunit3  48470  resum2sqgt0  48696  amgmwlem  49791