Theorem eqbrtrid 5120

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 2736	. 2 ⊢ 𝐶 = 𝐶
4	1, 2, 3	3brtr4g 5119	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  map1  8987  xp1en  9001  map2xp  9085  rex2dom  9163  sucxpdom  9171  sniffsupp  9313  wdomima2g  9501  endjudisj  10091  dju1dif  10095  mapdjuen  10103  djuxpdom  10108  djufi  10109  pwsdompw  10125  infunsdom1  10134  infunsdom  10135  infxp  10136  ackbij1lem5  10145  hsmexlem4  10351  imadomg  10456  unidom  10465  unictb  10498  pwxpndom2  10588  pwdjundom  10590  distrnq  10884  nnne0  12211  supxrmnf  13269  xov1plusxeqvd  13451  quoremz  13814  quoremnn0ALT  13816  intfrac2  13817  m1modge3gt1  13880  bernneq2  14192  faclbnd4lem1  14255  01sqrexlem4  15207  reccn2  15559  caucvg  15641  o1fsum  15776  infcvgaux2i  15823  eirrlem  16171  rpnnen2lem12  16192  ruclem12  16208  nno  16351  divalglem5  16366  bitsfzolem  16403  bitsinv1lem  16410  bezoutlem3  16510  lcmfunsnlem  16610  coprmproddvds  16632  oddprmge3  16670  ge2nprmge4  16671  sqnprm  16672  prmreclem6  16892  4sqlem6  16914  4sqlem13  16928  4sqlem16  16931  4sqlem17  16932  2expltfac  17063  odcau  19579  sylow3  19608  efginvrel2  19702  lt6abl  19870  ablfac1lem  20045  gzrngunitlem  21412  zringlpirlem3  21444  dvdschrmulg  21508  znfld  21540  evlslem2  22057  chfacffsupp  22821  cpmidpmatlem3  22837  cctop  22971  csdfil  23859  xpsdsval  24346  nrginvrcnlem  24656  icccmplem2  24789  reconnlem2  24793  iscmet3lem3  25257  minveclem2  25393  minveclem4  25399  ivthlem2  25419  ivthlem3  25420  ovolunlem1a  25463  ovolfiniun  25468  ovoliunlem3  25471  ovoliun  25472  ovolicc2lem4  25487  unmbl  25504  ioombl1lem4  25528  itg2mono  25720  ibladdlem  25787  iblabsr  25797  iblmulc2  25798  bddiblnc  25809  dvferm1lem  25951  dvferm2lem  25953  lhop1lem  25980  dvcvx  25987  ftc1a  26004  plyeq0lem  26175  aannenlem3  26296  geolim3  26305  psercnlem1  26390  pserdvlem2  26393  reeff1olem  26411  pilem2  26417  pilem3  26418  cosq14gt0  26474  cosq14ge0  26475  cosne0  26493  recosf1o  26499  resinf1o  26500  argregt0  26574  logcnlem3  26608  logcnlem4  26609  logf1o2  26614  cxpcn3lem  26711  ang180lem2  26774  acosbnd  26864  atanbndlem  26889  leibpi  26906  cxp2lim  26940  emcllem2  26960  ftalem5  27040  basellem9  27052  vmage0  27084  chpge0  27089  chtub  27175  mersenne  27190  bposlem2  27248  bposlem5  27251  bposlem6  27252  bposlem9  27255  gausslemma2dlem0c  27321  gausslemma2dlem0e  27323  lgseisenlem1  27338  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  mulog2sumlem2  27498  pntpbnd1a  27548  pntibndlem1  27552  pntibndlem3  27555  pntlemc  27558  ostth2  27600  ostth3  27601  absmuls  28236  pthdlem1  29834  numclwlk1lem2  30440  smcnlem  30768  minvecolem2  30946  minvecolem4  30951  strlem5  32326  hstrlem5  32334  abrexdomjm  32577  prct  32786  cyc3conja  33218  elrgspnlem2  33304  prmidl0  33510  mplvrpmga  33689  psrmonprod  33696  fldextrspunlsplem  33817  constrext2chnlem  33894  dya2icoseg  34421  omssubadd  34444  omsmeas  34467  oddpwdc  34498  logdivsqrle  34794  faclim  35928  faclim2  35930  taupilem1  37635  mblfinlem3  37980  mblfinlem4  37981  ibladdnclem  37997  iblmulc2nc  38006  abrexdom  38051  dalem3  40110  dalem8  40116  dalem25  40144  dalem27  40145  dalem38  40156  dalem44  40162  dalem54  40172  lhpat3  40492  4atexlemunv  40512  4atexlemtlw  40513  4atexlemc  40515  4atexlemnclw  40516  4atexlemex2  40517  4atexlemcnd  40518  cdleme0b  40658  cdleme0c  40659  cdleme0fN  40664  cdlemeulpq  40666  cdleme01N  40667  cdleme0ex1N  40669  cdleme2  40674  cdleme3b  40675  cdleme3c  40676  cdleme3g  40680  cdleme3h  40681  cdleme4a  40685  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme9  40699  cdleme11fN  40710  cdleme11k  40714  cdleme15d  40723  cdlemednpq  40745  cdleme19c  40751  cdleme20aN  40755  cdleme20e  40759  cdleme21c  40773  cdleme21ct  40775  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme23a  40795  cdleme28a  40816  cdleme35f  40900  cdlemeg46frv  40971  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg6c  41066  cdlemg31a  41143  cdlemg31b  41144  cdlemk10  41289  cdlemk37  41360  dia2dimlem1  41510  dihjatcclem4  41867  imadomfi  42441  aks5lem1  42625  3cubeslem1  43116  irrapxlem3  43252  pell14qrgapw  43304  dgrsub2  43563  radcnvrat  44741  ressiooinf  45987  fmul01  46010  fmul01lt1lem1  46014  fmul01lt1lem2  46015  sumnnodd  46060  climlimsupcex  46197  cnrefiisplem  46257  stoweidlem1  46429  stoweidlem5  46433  stoweidlem7  46435  dirkercncflem1  46531  dirkercncflem4  46534  fourierdlem30  46565  fourierdlem42  46577  fourierdlem48  46582  fourierdlem62  46596  fourierdlem63  46597  fourierdlem68  46602  fourierdlem79  46613  sqwvfoura  46656  etransclem32  46694  hoidmvlelem2  47024  iunhoiioolem  47103  vonioolem1  47108  pimdecfgtioo  47145  pimincfltioo  47146  smfmullem1  47219  2ltceilhalf  47780  rehalfge1  47787  m1modnep2mod  47806  difmodm1lt  47813  2timesltsqm1  47827  fmtnoge3  47993  fmtnoprmfac2lem1  48029  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem4a  48071  proththdlem  48076  nprmdvdsfacm1lem2  48084  stgoldbwt  48252  sgoldbeven3prm  48259  mogoldbb  48261  evengpop3  48274  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  lindslinindimp2lem3  48936  fllogbd  49036  nnolog2flm1  49066