Theorem breqtrrdi 5144

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 5143	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  enpr2d  8997  enpr2dOLD  8998  pw2eng  9024  undjudom  10097  dju1en  10101  djucomen  10107  djuassen  10108  xpdjuen  10109  infdjuabs  10134  ackbij1lem9  10156  unsnen  10482  1nqenq  10891  gtndiv  12587  xov1plusxeqvd  13435  intfrac2  13796  serle  13998  discr1  14180  faclbnd4lem1  14234  01sqrexlem1  15184  01sqrexlem4  15187  01sqrexlem7  15190  supcvg  15798  ege2le3  16032  eirrlem  16148  ruclem12  16185  bitsfzo  16381  pcprendvds  16787  pcpremul  16790  pcfaclem  16845  infpnlem2  16858  yonedainv  18222  srgbinomlem4  20149  lmcn2  23569  hmph0  23715  icccmplem2  24745  reconnlem2  24749  xrge0tsms  24756  minveclem2  25359  minveclem3b  25361  minveclem4  25365  minveclem6  25367  ivthlem2  25386  ivthlem3  25387  vitalilem2  25543  itg2seq  25676  itg2monolem1  25684  itg2monolem2  25685  itg2monolem3  25686  dveflem  25916  dvferm1lem  25921  dvferm2lem  25923  c1liplem1  25934  lhop1lem  25951  dvcvx  25958  plyeq0lem  26148  radcnvcl  26359  radcnvle  26362  psercnlem1  26368  psercn  26369  pilem3  26396  tangtx  26447  cos02pilt1  26468  cosne0  26471  recosf1o  26477  resinf1o  26478  efif1olem4  26487  logi  26529  logimul  26556  logcnlem3  26586  logf1o2  26592  ang180lem2  26753  heron  26781  acoscos  26836  emcllem7  26945  fsumharmonic  26955  ftalem2  27017  basellem1  27024  basellem2  27025  basellem3  27026  basellem5  27028  bposlem1  27228  bposlem2  27229  bposlem3  27230  lgsdirprm  27275  chebbnd1lem1  27413  chebbnd1lem2  27414  chebbnd1lem3  27415  mulog2sumlem2  27479  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2  27535  pntlemc  27539  pntlemb  27541  pntlemg  27542  pntlemh  27543  pntlemr  27546  ostth2lem2  27578  ostth2lem3  27579  ostth2lem4  27580  ostth3  27582  axsegconlem3  28899  clwlkclwwlk2  29982  siilem1  30830  minvecolem2  30854  minvecolem4  30859  minvecolem5  30860  minvecolem6  30861  nmopcoi  32074  staddi  32225  cycpmco2lem4  33101  cycpmco2lem5  33102  iconstr  33749  hgt750lemd  34632  climlec3  35714  poimirlem26  37633  ftc1anclem8  37687  cntotbnd  37783  dalemply  39641  dalemsly  39642  dalem5  39654  dalem13  39663  dalem17  39667  dalem55  39714  dalem57  39716  lhpat3  40033  cdleme22aa  40326  aks4d1p1p7  42055  evlselv  42568  jm2.27c  42989  hashnzfz2  44303  supxrubd  45100  suprnmpt  45161  fzisoeu  45291  upbdrech  45296  recnnltrp  45366  uzublem  45419  fmul01  45571  limsupubuzlem  45703  limsupequzmptlem  45719  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem36  46027  stoweidlem41  46032  wallispi2  46064  dirkercncflem1  46094  fourierdlem6  46104  fourierdlem7  46105  fourierdlem19  46117  fourierdlem20  46118  fourierdlem24  46122  fourierdlem25  46123  fourierdlem26  46124  fourierdlem30  46128  fourierdlem31  46129  fourierdlem42  46140  fourierdlem47  46144  fourierdlem48  46145  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem71  46168  fourierdlem79  46176  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fouriersw  46222  etransclem28  46253  etransclem48  46273  hoidmv1lelem1  46582  hoidmv1lelem3  46584  hoidmvlelem1  46586  hoidmvlelem4  46589  bgoldbtbndlem2  47800  gpg3kgrtriexlem4  48070  gpg3kgrtriexlem6  48072  lincresunit3lem2  48462  lincresunit3  48463  resum2sqgt0  48689  amgmwlem  49784