Theorem eqbrtrid 5121

Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)

Hypotheses

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

Assertion

Ref	Expression
eqbrtrid	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrid

Step	Hyp	Ref	Expression
1		eqbrtrid.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrid.1	. 2 ⊢ 𝐴 = 𝐵
3		eqid 2731	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr4g 5120	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087

This theorem is referenced by:  map1  8957  xp1en  8971  map2xp  9055  rex2dom  9132  sucxpdom  9140  sniffsupp  9279  wdomima2g  9467  endjudisj  10055  dju1dif  10059  mapdjuen  10067  djuxpdom  10072  djufi  10073  pwsdompw  10089  infunsdom1  10098  infunsdom  10099  infxp  10100  ackbij1lem5  10109  hsmexlem4  10315  imadomg  10420  unidom  10429  unictb  10461  pwxpndom2  10551  pwdjundom  10553  distrnq  10847  nnne0  12154  supxrmnf  13211  xov1plusxeqvd  13393  quoremz  13754  quoremnn0ALT  13756  intfrac2  13757  m1modge3gt1  13820  bernneq2  14132  faclbnd4lem1  14195  01sqrexlem4  15147  reccn2  15499  caucvg  15581  o1fsum  15715  infcvgaux2i  15760  eirrlem  16108  rpnnen2lem12  16129  ruclem12  16145  nno  16288  divalglem5  16303  bitsfzolem  16340  bitsinv1lem  16347  bezoutlem3  16447  lcmfunsnlem  16547  coprmproddvds  16569  oddprmge3  16606  ge2nprmge4  16607  sqnprm  16608  prmreclem6  16828  4sqlem6  16850  4sqlem13  16864  4sqlem16  16867  4sqlem17  16868  2expltfac  16999  odcau  19511  sylow3  19540  efginvrel2  19634  lt6abl  19802  ablfac1lem  19977  gzrngunitlem  21364  zringlpirlem3  21396  dvdschrmulg  21460  znfld  21492  evlslem2  22009  chfacffsupp  22766  cpmidpmatlem3  22782  cctop  22916  csdfil  23804  xpsdsval  24291  nrginvrcnlem  24601  icccmplem2  24734  reconnlem2  24738  iscmet3lem3  25212  minveclem2  25348  minveclem4  25354  ivthlem2  25375  ivthlem3  25376  ovolunlem1a  25419  ovolfiniun  25424  ovoliunlem3  25427  ovoliun  25428  ovolicc2lem4  25443  unmbl  25460  ioombl1lem4  25484  itg2mono  25676  ibladdlem  25743  iblabsr  25753  iblmulc2  25754  bddiblnc  25765  dvferm1lem  25910  dvferm2lem  25912  lhop1lem  25940  dvcvx  25947  ftc1a  25966  plyeq0lem  26137  aannenlem3  26260  geolim3  26269  psercnlem1  26357  pserdvlem2  26360  reeff1olem  26378  pilem2  26384  pilem3  26385  cosq14gt0  26441  cosq14ge0  26442  cosne0  26460  recosf1o  26466  resinf1o  26467  argregt0  26541  logcnlem3  26575  logcnlem4  26576  logf1o2  26581  cxpcn3lem  26679  ang180lem2  26742  acosbnd  26832  atanbndlem  26857  leibpi  26874  cxp2lim  26909  emcllem2  26929  ftalem5  27009  basellem9  27021  vmage0  27053  chpge0  27058  chtub  27145  mersenne  27160  bposlem2  27218  bposlem5  27221  bposlem6  27222  bposlem9  27225  gausslemma2dlem0c  27291  gausslemma2dlem0e  27293  lgseisenlem1  27308  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  chebbnd1lem1  27402  chebbnd1lem2  27403  chebbnd1lem3  27404  mulog2sumlem2  27468  pntpbnd1a  27518  pntibndlem1  27522  pntibndlem3  27525  pntlemc  27528  ostth2  27570  ostth3  27571  absmuls  28177  pthdlem1  29739  numclwlk1lem2  30342  smcnlem  30669  minvecolem2  30847  minvecolem4  30852  strlem5  32227  hstrlem5  32235  abrexdomjm  32479  prct  32688  cyc3conja  33118  elrgspnlem2  33202  prmidl0  33407  mplvrpmga  33567  fldextrspunlsplem  33678  constrext2chnlem  33755  dya2icoseg  34282  omssubadd  34305  omsmeas  34328  oddpwdc  34359  logdivsqrle  34655  faclim  35782  faclim2  35784  taupilem1  37355  mblfinlem3  37699  mblfinlem4  37700  ibladdnclem  37716  iblmulc2nc  37725  abrexdom  37770  dalem3  39703  dalem8  39709  dalem25  39737  dalem27  39738  dalem38  39749  dalem44  39755  dalem54  39765  lhpat3  40085  4atexlemunv  40105  4atexlemtlw  40106  4atexlemc  40108  4atexlemnclw  40109  4atexlemex2  40110  4atexlemcnd  40111  cdleme0b  40251  cdleme0c  40252  cdleme0fN  40257  cdlemeulpq  40259  cdleme01N  40260  cdleme0ex1N  40262  cdleme2  40267  cdleme3b  40268  cdleme3c  40269  cdleme3g  40273  cdleme3h  40274  cdleme4a  40278  cdleme7aa  40281  cdleme7c  40284  cdleme7d  40285  cdleme7e  40286  cdleme9  40292  cdleme11fN  40303  cdleme11k  40307  cdleme15d  40316  cdlemednpq  40338  cdleme19c  40344  cdleme20aN  40348  cdleme20e  40352  cdleme21c  40366  cdleme21ct  40368  cdleme22e  40383  cdleme22eALTN  40384  cdleme22f  40385  cdleme23a  40388  cdleme28a  40409  cdleme35f  40493  cdlemeg46frv  40564  cdlemeg46rgv  40567  cdlemeg46req  40568  cdlemg2fv2  40639  cdlemg2m  40643  cdlemg6c  40659  cdlemg31a  40736  cdlemg31b  40737  cdlemk10  40882  cdlemk37  40953  dia2dimlem1  41103  dihjatcclem4  41460  imadomfi  42035  aks5lem1  42219  3cubeslem1  42717  irrapxlem3  42857  pell14qrgapw  42909  dgrsub2  43168  radcnvrat  44347  ressiooinf  45597  fmul01  45620  fmul01lt1lem1  45624  fmul01lt1lem2  45625  sumnnodd  45670  climlimsupcex  45807  cnrefiisplem  45867  stoweidlem1  46039  stoweidlem5  46043  stoweidlem7  46045  dirkercncflem1  46141  dirkercncflem4  46144  fourierdlem30  46175  fourierdlem42  46187  fourierdlem48  46192  fourierdlem62  46206  fourierdlem63  46207  fourierdlem68  46212  fourierdlem79  46223  sqwvfoura  46266  etransclem32  46304  hoidmvlelem2  46634  iunhoiioolem  46713  vonioolem1  46718  pimdecfgtioo  46755  pimincfltioo  46756  smfmullem1  46829  2ltceilhalf  47359  rehalfge1  47366  m1modnep2mod  47383  difmodm1lt  47390  fmtnoge3  47561  fmtnoprmfac2lem1  47597  sfprmdvdsmersenne  47634  lighneallem2  47637  lighneallem4a  47639  proththdlem  47644  stgoldbwt  47807  sgoldbeven3prm  47814  mogoldbb  47816  evengpop3  47829  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  lindslinindimp2lem3  48492  fllogbd  48592  nnolog2flm1  48622