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

Syntax hints:   → wi 4   = wceq 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  map1  8980  xp1en  8994  map2xp  9078  rex2dom  9156  sucxpdom  9164  sniffsupp  9306  wdomima2g  9494  endjudisj  10082  dju1dif  10086  mapdjuen  10094  djuxpdom  10099  djufi  10100  pwsdompw  10116  infunsdom1  10125  infunsdom  10126  infxp  10127  ackbij1lem5  10136  hsmexlem4  10342  imadomg  10447  unidom  10456  unictb  10489  pwxpndom2  10579  pwdjundom  10581  distrnq  10875  nnne0  12202  supxrmnf  13260  xov1plusxeqvd  13442  quoremz  13805  quoremnn0ALT  13807  intfrac2  13808  m1modge3gt1  13871  bernneq2  14183  faclbnd4lem1  14246  01sqrexlem4  15198  reccn2  15550  caucvg  15632  o1fsum  15767  infcvgaux2i  15814  eirrlem  16162  rpnnen2lem12  16183  ruclem12  16199  nno  16342  divalglem5  16357  bitsfzolem  16394  bitsinv1lem  16401  bezoutlem3  16501  lcmfunsnlem  16601  coprmproddvds  16623  oddprmge3  16661  ge2nprmge4  16662  sqnprm  16663  prmreclem6  16883  4sqlem6  16905  4sqlem13  16919  4sqlem16  16922  4sqlem17  16923  2expltfac  17054  odcau  19570  sylow3  19599  efginvrel2  19693  lt6abl  19861  ablfac1lem  20036  gzrngunitlem  21422  zringlpirlem3  21454  dvdschrmulg  21518  znfld  21550  evlslem2  22067  chfacffsupp  22831  cpmidpmatlem3  22847  cctop  22981  csdfil  23869  xpsdsval  24356  nrginvrcnlem  24666  icccmplem2  24799  reconnlem2  24803  iscmet3lem3  25267  minveclem2  25403  minveclem4  25409  ivthlem2  25429  ivthlem3  25430  ovolunlem1a  25473  ovolfiniun  25478  ovoliunlem3  25481  ovoliun  25482  ovolicc2lem4  25497  unmbl  25514  ioombl1lem4  25538  itg2mono  25730  ibladdlem  25797  iblabsr  25807  iblmulc2  25808  bddiblnc  25819  dvferm1lem  25961  dvferm2lem  25963  lhop1lem  25990  dvcvx  25997  ftc1a  26014  plyeq0lem  26185  aannenlem3  26307  geolim3  26316  psercnlem1  26403  pserdvlem2  26406  reeff1olem  26424  pilem2  26430  pilem3  26431  cosq14gt0  26487  cosq14ge0  26488  cosne0  26506  recosf1o  26512  resinf1o  26513  argregt0  26587  logcnlem3  26621  logcnlem4  26622  logf1o2  26627  cxpcn3lem  26724  ang180lem2  26787  acosbnd  26877  atanbndlem  26902  leibpi  26919  cxp2lim  26954  emcllem2  26974  ftalem5  27054  basellem9  27066  vmage0  27098  chpge0  27103  chtub  27189  mersenne  27204  bposlem2  27262  bposlem5  27265  bposlem6  27266  bposlem9  27269  gausslemma2dlem0c  27335  gausslemma2dlem0e  27337  lgseisenlem1  27352  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  chebbnd1lem1  27446  chebbnd1lem2  27447  chebbnd1lem3  27448  mulog2sumlem2  27512  pntpbnd1a  27562  pntibndlem1  27566  pntibndlem3  27569  pntlemc  27572  ostth2  27614  ostth3  27615  absmuls  28250  pthdlem1  29849  numclwlk1lem2  30455  smcnlem  30783  minvecolem2  30961  minvecolem4  30966  strlem5  32341  hstrlem5  32349  abrexdomjm  32592  prct  32801  cyc3conja  33233  elrgspnlem2  33319  prmidl0  33525  mplvrpmga  33704  psrmonprod  33711  fldextrspunlsplem  33833  constrext2chnlem  33910  dya2icoseg  34437  omssubadd  34460  omsmeas  34483  oddpwdc  34514  logdivsqrle  34810  faclim  35944  faclim2  35946  taupilem1  37651  mblfinlem3  37994  mblfinlem4  37995  ibladdnclem  38011  iblmulc2nc  38020  abrexdom  38065  dalem3  40124  dalem8  40130  dalem25  40158  dalem27  40159  dalem38  40170  dalem44  40176  dalem54  40186  lhpat3  40506  4atexlemunv  40526  4atexlemtlw  40527  4atexlemc  40529  4atexlemnclw  40530  4atexlemex2  40531  4atexlemcnd  40532  cdleme0b  40672  cdleme0c  40673  cdleme0fN  40678  cdlemeulpq  40680  cdleme01N  40681  cdleme0ex1N  40683  cdleme2  40688  cdleme3b  40689  cdleme3c  40690  cdleme3g  40694  cdleme3h  40695  cdleme4a  40699  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme9  40713  cdleme11fN  40724  cdleme11k  40728  cdleme15d  40737  cdlemednpq  40759  cdleme19c  40765  cdleme20aN  40769  cdleme20e  40773  cdleme21c  40787  cdleme21ct  40789  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme23a  40809  cdleme28a  40830  cdleme35f  40914  cdlemeg46frv  40985  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg6c  41080  cdlemg31a  41157  cdlemg31b  41158  cdlemk10  41303  cdlemk37  41374  dia2dimlem1  41524  dihjatcclem4  41881  imadomfi  42455  aks5lem1  42639  3cubeslem1  43130  irrapxlem3  43270  pell14qrgapw  43322  dgrsub2  43581  radcnvrat  44759  ressiooinf  46005  fmul01  46028  fmul01lt1lem1  46032  fmul01lt1lem2  46033  sumnnodd  46078  climlimsupcex  46215  cnrefiisplem  46275  stoweidlem1  46447  stoweidlem5  46451  stoweidlem7  46453  dirkercncflem1  46549  dirkercncflem4  46552  fourierdlem30  46583  fourierdlem42  46595  fourierdlem48  46600  fourierdlem62  46614  fourierdlem63  46615  fourierdlem68  46620  fourierdlem79  46631  sqwvfoura  46674  etransclem32  46712  hoidmvlelem2  47042  iunhoiioolem  47121  vonioolem1  47126  pimdecfgtioo  47163  pimincfltioo  47164  smfmullem1  47237  2ltceilhalf  47792  rehalfge1  47799  m1modnep2mod  47818  difmodm1lt  47825  2timesltsqm1  47839  fmtnoge3  48005  fmtnoprmfac2lem1  48041  sfprmdvdsmersenne  48078  lighneallem2  48081  lighneallem4a  48083  proththdlem  48088  nprmdvdsfacm1lem2  48096  stgoldbwt  48264  sgoldbeven3prm  48271  mogoldbb  48273  evengpop3  48286  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  lindslinindimp2lem3  48948  fllogbd  49048  nnolog2flm1  49078