Theorem eqbrtrid 5146

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109

This theorem is used by:  map1  9106  xp1en  9120  map2xp  9204  rex2dom  9282  sucxpdom  9290  sniffsupp  9429  wdomima2g  9617  endjudisj  10286  dju1dif  10290  mapdjuen  10298  djuxpdom  10303  djufi  10304  pwsdompw  10320  infunsdom1  10329  infunsdom  10330  infxp  10331  ackbij1lem5  10340  hsmexlem4  10546  imadomg  10652  imadomnum  10653  unidom  10666  unictb  10699  pwxpndom2  10789  pwdjundom  10791  distrnq  11085  nnne0  12412  supxrmnf  13487  xov1plusxeqvd  13669  quoremz  14035  quoremnn0ALT  14037  intfrac2  14038  m1modge3gt1  14101  bernneq2  14415  faclbnd4lem1  14478  01sqrexlem4  15455  reccn2  15808  caucvg  15890  o1fsum  16024  infcvgaux2i  16071  eirrlem  16416  rpnnen2lem12  16437  ruclem12  16453  nno  16596  divalglem5  16611  bitsfzolem  16648  bitsinv1lem  16655  bezoutlem3  16758  lcmfunsnlem  16860  coprmproddvds  16882  oddprmge3  16920  ge2nprmge4  16921  sqnprm  16922  prmreclem6  17143  4sqlem6  17165  4sqlem13  17179  4sqlem16  17182  4sqlem17  17183  2expltfac  17314  odcau  19869  sylow3  19898  efginvrel2  19992  lt6abl  20160  ablfac1lem  20335  prmidl0  21685  gzrngunitlem  21792  zringlpirlem3  21825  dvdschrmulg  21889  znfld  21921  evlslem2  22443  chfacffsupp  23229  cpmidpmatlem3  23245  cctop  23379  csdfil  24268  xpsdsval  24755  nrginvrcnlem  25065  icccmplem2  25198  reconnlem2  25202  iscmet3lem3  25666  minveclem2  25802  minveclem4  25808  ivthlem2  25828  ivthlem3  25829  ovolunlem1a  25872  ovolfiniun  25877  ovoliunlem3  25880  ovoliun  25881  ovolicc2lem4  25896  unmbl  25913  ioombl1lem4  25937  itg2mono  26129  ibladdlem  26195  iblabsr  26205  iblmulc2  26206  bddiblnc  26217  dvferm1lem  26359  dvferm2lem  26361  lhop1lem  26388  dvcvx  26395  ftc1a  26412  plyeq0lem  26584  aannenlem3  26714  geolim3  26723  psercnlem1  26809  pserdvlem2  26812  reeff1olem  26830  pilem2  26836  pilem3  26837  cosq14gt0  26896  cosq14ge0  26897  cosne0  26914  recosf1o  26920  resinf1o  26921  argregt0  26995  logcnlem3  27029  logcnlem4  27030  logf1o2  27035  cxpcn3lem  27132  ang180lem2  27195  acosbnd  27285  atanbndlem  27310  leibpi  27327  cxp2lim  27361  emcllem2  27381  ftalem5  27461  basellem9  27473  vmage0  27505  chpge0  27510  chtub  27596  mersenne  27611  bposlem2  27669  bposlem5  27672  bposlem6  27673  bposlem9  27676  gausslemma2dlem0c  27742  gausslemma2dlem0e  27744  lgseisenlem1  27759  lgsquadlem1  27764  lgsquadlem2  27765  lgsquadlem3  27766  chebbnd1lem1  27853  chebbnd1lem2  27854  chebbnd1lem3  27855  mulog2sumlem2  27919  pntpbnd1a  27969  pntibndlem1  27973  pntibndlem3  27976  pntlemc  27979  ostth2  28021  ostth3  28022  fltoprmlem2  28051  absmuls  28687  pthdlem1  30409  numclwlk1lem2  31028  smcnlem  31356  minvecolem2  31534  minvecolem4  31539  strlem5  32914  hstrlem5  32922  abrexdomjm  33202  prct  33403  cyc3conja  33817  elrgspnlem2  33903  mplvrpmga  34288  psrmonprod  34295  fldextrspunlsplem  34416  constrext2chnlem  34493  dya2icoseg  35020  omssubadd  35043  omsmeas  35066  oddpwdc  35097  logdivsqrle  35390  faclim  36726  faclim2  36728  taupilem1  38510  mblfinlem3  38845  mblfinlem4  38846  ibladdnclem  38862  iblmulc2nc  38871  abrexdom  38932  dalem3  40987  dalem8  40993  dalem25  41021  dalem27  41022  dalem38  41033  dalem44  41039  dalem54  41049  lhpat3  41369  4atexlemunv  41389  4atexlemtlw  41390  4atexlemc  41392  4atexlemnclw  41393  4atexlemex2  41394  4atexlemcnd  41395  cdleme0b  41535  cdleme0c  41536  cdleme0fN  41541  cdlemeulpq  41543  cdleme01N  41544  cdleme0ex1N  41546  cdleme2  41551  cdleme3b  41552  cdleme3c  41553  cdleme3g  41557  cdleme3h  41558  cdleme4a  41562  cdleme7aa  41565  cdleme7c  41568  cdleme7d  41569  cdleme7e  41570  cdleme9  41576  cdleme11fN  41587  cdleme11k  41591  cdleme15d  41600  cdlemednpq  41622  cdleme19c  41628  cdleme20aN  41632  cdleme20e  41636  cdleme21c  41650  cdleme21ct  41652  cdleme22e  41667  cdleme22eALTN  41668  cdleme22f  41669  cdleme23a  41672  cdleme28a  41693  cdleme35f  41777  cdlemeg46frv  41848  cdlemeg46rgv  41851  cdlemeg46req  41852  cdlemg2fv2  41923  cdlemg2m  41927  cdlemg6c  41943  cdlemg31a  42020  cdlemg31b  42021  cdlemk10  42166  cdlemk37  42237  dia2dimlem1  42387  dihjatcclem4  42744  imadomfi  43318  aks5lem1  43502  3cubeslem1  43960  irrapxlem3  44097  pell14qrgapw  44149  dgrsub2  44402  radcnvrat  45559  ressiooinf  46842  fmul01  46865  fmul01lt1lem1  46869  fmul01lt1lem2  46870  sumnnodd  46915  climlimsupcex  47052  cnrefiisplem  47112  stoweidlem1  47284  stoweidlem5  47288  stoweidlem7  47290  dirkercncflem1  47386  dirkercncflem4  47389  fourierdlem30  47420  fourierdlem42  47432  fourierdlem48  47437  fourierdlem49  47438  fourierdlem62  47451  fourierdlem63  47452  fourierdlem68  47457  fourierdlem79  47468  sqwvfoura  47511  etransclem32  47549  hoidmvlelem2  47879  iunhoiioolem  47958  vonioolem1  47963  pimdecfgtioo  48000  pimincfltioo  48001  smfmullem1  48074  2ltceilhalf  48675  rehalfge1  48682  m1modnep2mod  48701  difmodm1lt  48708  2timesltsqm1  48722  fmtnoge3  48888  fmtnoprmfac2lem1  48924  sfprmdvdsmersenne  48961  lighneallem2  48964  lighneallem4a  48966  proththdlem  48971  nprmdvdsfacm1lem2  48979  stgoldbwt  49147  sgoldbeven3prm  49154  mogoldbb  49156  evengpop3  49169  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  lindslinindimp2lem3  49903  fllogbd  50003  nnolog2flm1  50033