Theorem eqbrtrid 5072

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3866  df-sn 4527  df-pr 4529  df-op 4533  df-br 5038

This theorem is referenced by:  map1  8625  xp1en  8638  map2xp  8723  1sdom  8773  sucxpdom  8779  sniffsupp  8911  wdomima2g  9097  endjudisj  9642  dju1dif  9646  mapdjuen  9654  djuxpdom  9659  djufi  9660  pwsdompw  9678  infunsdom1  9687  infunsdom  9688  infxp  9689  ackbij1lem5  9698  hsmexlem4  9903  imadomg  10008  unidom  10017  unictb  10049  pwxpndom2  10139  pwdjundom  10141  distrnq  10435  nnne0  11722  supxrmnf  12765  xov1plusxeqvd  12944  quoremz  13286  quoremnn0ALT  13288  intfrac2  13289  m1modge3gt1  13349  bernneq2  13655  faclbnd4lem1  13717  sqrlem4  14667  reccn2  15015  caucvg  15097  o1fsum  15230  infcvgaux2i  15275  eirrlem  15619  rpnnen2lem12  15640  ruclem12  15656  nno  15797  divalglem5  15812  bitsfzolem  15847  bitsinv1lem  15854  bezoutlem3  15955  lcmfunsnlem  16052  coprmproddvds  16074  oddprmge3  16111  ge2nprmge4  16112  sqnprm  16113  prmreclem6  16327  4sqlem6  16349  4sqlem13  16363  4sqlem16  16366  4sqlem17  16367  2expltfac  16499  odcau  18811  sylow3  18840  efginvrel2  18935  lt6abl  19098  ablfac1lem  19273  gzrngunitlem  20246  zringlpirlem3  20269  znfld  20343  evlslem2  20857  chfacffsupp  21571  cpmidpmatlem3  21587  cctop  21721  csdfil  22609  xpsdsval  23098  nrginvrcnlem  23408  icccmplem2  23539  reconnlem2  23543  iscmet3lem3  24005  minveclem2  24141  minveclem4  24147  ivthlem2  24167  ivthlem3  24168  ovolunlem1a  24211  ovolfiniun  24216  ovoliunlem3  24219  ovoliun  24220  ovolicc2lem4  24235  unmbl  24252  ioombl1lem4  24276  itg2mono  24468  ibladdlem  24534  iblabsr  24544  iblmulc2  24545  bddiblnc  24556  dvferm1lem  24698  dvferm2lem  24700  lhop1lem  24727  dvcvx  24734  ftc1a  24751  plyeq0lem  24921  aannenlem3  25040  geolim3  25049  psercnlem1  25134  pserdvlem2  25137  reeff1olem  25155  pilem2  25161  pilem3  25162  cosq14gt0  25217  cosq14ge0  25218  cosne0  25235  recosf1o  25241  resinf1o  25242  argregt0  25315  logcnlem3  25349  logcnlem4  25350  logf1o2  25355  cxpcn3lem  25450  ang180lem2  25510  acosbnd  25600  atanbndlem  25625  leibpi  25642  cxp2lim  25676  emcllem2  25696  ftalem5  25776  basellem9  25788  vmage0  25820  chpge0  25825  chtub  25910  mersenne  25925  bposlem2  25983  bposlem5  25986  bposlem6  25987  bposlem9  25990  gausslemma2dlem0c  26056  gausslemma2dlem0e  26058  lgseisenlem1  26073  lgsquadlem1  26078  lgsquadlem2  26079  lgsquadlem3  26080  chebbnd1lem1  26167  chebbnd1lem2  26168  chebbnd1lem3  26169  mulog2sumlem2  26233  pntpbnd1a  26283  pntibndlem1  26287  pntibndlem3  26290  pntlemc  26293  ostth2  26335  ostth3  26336  pthdlem1  27669  numclwlk1lem2  28269  smcnlem  28594  minvecolem2  28772  minvecolem4  28777  strlem5  30152  hstrlem5  30160  abrexdomjm  30389  prct  30587  cyc3conja  30964  dvdschrmulg  31023  prmidl0  31161  dya2icoseg  31777  omssubadd  31800  omsmeas  31823  oddpwdc  31854  logdivsqrle  32163  faclim  33241  faclim2  33243  taupilem1  35051  mblfinlem3  35412  mblfinlem4  35413  ibladdnclem  35429  iblmulc2nc  35438  abrexdom  35484  dalem3  37276  dalem8  37282  dalem25  37310  dalem27  37311  dalem38  37322  dalem44  37328  dalem54  37338  lhpat3  37658  4atexlemunv  37678  4atexlemtlw  37679  4atexlemc  37681  4atexlemnclw  37682  4atexlemex2  37683  4atexlemcnd  37684  cdleme0b  37824  cdleme0c  37825  cdleme0fN  37830  cdlemeulpq  37832  cdleme01N  37833  cdleme0ex1N  37835  cdleme2  37840  cdleme3b  37841  cdleme3c  37842  cdleme3g  37846  cdleme3h  37847  cdleme4a  37851  cdleme7aa  37854  cdleme7c  37857  cdleme7d  37858  cdleme7e  37859  cdleme9  37865  cdleme11fN  37876  cdleme11k  37880  cdleme15d  37889  cdlemednpq  37911  cdleme19c  37917  cdleme20aN  37921  cdleme20e  37925  cdleme21c  37939  cdleme21ct  37941  cdleme22e  37956  cdleme22eALTN  37957  cdleme22f  37958  cdleme23a  37961  cdleme28a  37982  cdleme35f  38066  cdlemeg46frv  38137  cdlemeg46rgv  38140  cdlemeg46req  38141  cdlemg2fv2  38212  cdlemg2m  38216  cdlemg6c  38232  cdlemg31a  38309  cdlemg31b  38310  cdlemk10  38455  cdlemk37  38526  dia2dimlem1  38676  dihjatcclem4  39033  metakunt30  39712  3cubeslem1  40044  irrapxlem3  40184  pell14qrgapw  40236  dgrsub2  40498  radcnvrat  41437  ressiooinf  42606  fmul01  42634  fmul01lt1lem1  42638  fmul01lt1lem2  42639  sumnnodd  42684  climlimsupcex  42823  cnrefiisplem  42883  stoweidlem1  43055  stoweidlem5  43059  stoweidlem7  43061  dirkercncflem1  43157  dirkercncflem4  43160  fourierdlem30  43191  fourierdlem42  43203  fourierdlem48  43208  fourierdlem62  43222  fourierdlem63  43223  fourierdlem68  43228  fourierdlem79  43239  sqwvfoura  43282  etransclem32  43320  hoidmvlelem2  43647  iunhoiioolem  43726  vonioolem1  43731  pimdecfgtioo  43764  pimincfltioo  43765  smfmullem1  43835  fmtnoge3  44475  fmtnoprmfac2lem1  44511  sfprmdvdsmersenne  44548  lighneallem2  44551  lighneallem4a  44553  proththdlem  44558  stgoldbwt  44721  sgoldbeven3prm  44728  mogoldbb  44730  evengpop3  44743  bgoldbtbndlem2  44751  bgoldbtbndlem3  44752  lindslinindimp2lem3  45294  fllogbd  45399  nnolog2flm1  45429