Theorem eqbrtrid 5182

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  map1  9036  xp1en  9053  map2xp  9143  rex2dom  9242  1sdomOLD  9245  sucxpdom  9251  sniffsupp  9391  wdomima2g  9577  endjudisj  10159  dju1dif  10163  mapdjuen  10171  djuxpdom  10176  djufi  10177  pwsdompw  10195  infunsdom1  10204  infunsdom  10205  infxp  10206  ackbij1lem5  10215  hsmexlem4  10420  imadomg  10525  unidom  10534  unictb  10566  pwxpndom2  10656  pwdjundom  10658  distrnq  10952  nnne0  12242  supxrmnf  13292  xov1plusxeqvd  13471  quoremz  13816  quoremnn0ALT  13818  intfrac2  13819  m1modge3gt1  13879  bernneq2  14189  faclbnd4lem1  14249  01sqrexlem4  15188  reccn2  15537  caucvg  15621  o1fsum  15755  infcvgaux2i  15800  eirrlem  16143  rpnnen2lem12  16164  ruclem12  16180  nno  16321  divalglem5  16336  bitsfzolem  16371  bitsinv1lem  16378  bezoutlem3  16479  lcmfunsnlem  16574  coprmproddvds  16596  oddprmge3  16633  ge2nprmge4  16634  sqnprm  16635  prmreclem6  16850  4sqlem6  16872  4sqlem13  16886  4sqlem16  16889  4sqlem17  16890  2expltfac  17022  odcau  19466  sylow3  19495  efginvrel2  19589  lt6abl  19757  ablfac1lem  19932  gzrngunitlem  21002  zringlpirlem3  21025  znfld  21107  evlslem2  21633  chfacffsupp  22349  cpmidpmatlem3  22365  cctop  22500  csdfil  23389  xpsdsval  23878  nrginvrcnlem  24199  icccmplem2  24330  reconnlem2  24334  iscmet3lem3  24798  minveclem2  24934  minveclem4  24940  ivthlem2  24960  ivthlem3  24961  ovolunlem1a  25004  ovolfiniun  25009  ovoliunlem3  25012  ovoliun  25013  ovolicc2lem4  25028  unmbl  25045  ioombl1lem4  25069  itg2mono  25262  ibladdlem  25328  iblabsr  25338  iblmulc2  25339  bddiblnc  25350  dvferm1lem  25492  dvferm2lem  25494  lhop1lem  25521  dvcvx  25528  ftc1a  25545  plyeq0lem  25715  aannenlem3  25834  geolim3  25843  psercnlem1  25928  pserdvlem2  25931  reeff1olem  25949  pilem2  25955  pilem3  25956  cosq14gt0  26011  cosq14ge0  26012  cosne0  26029  recosf1o  26035  resinf1o  26036  argregt0  26109  logcnlem3  26143  logcnlem4  26144  logf1o2  26149  cxpcn3lem  26244  ang180lem2  26304  acosbnd  26394  atanbndlem  26419  leibpi  26436  cxp2lim  26470  emcllem2  26490  ftalem5  26570  basellem9  26582  vmage0  26614  chpge0  26619  chtub  26704  mersenne  26719  bposlem2  26777  bposlem5  26780  bposlem6  26781  bposlem9  26784  gausslemma2dlem0c  26850  gausslemma2dlem0e  26852  lgseisenlem1  26867  lgsquadlem1  26872  lgsquadlem2  26873  lgsquadlem3  26874  chebbnd1lem1  26961  chebbnd1lem2  26962  chebbnd1lem3  26963  mulog2sumlem2  27027  pntpbnd1a  27077  pntibndlem1  27081  pntibndlem3  27084  pntlemc  27087  ostth2  27129  ostth3  27130  pthdlem1  29012  numclwlk1lem2  29612  smcnlem  29937  minvecolem2  30115  minvecolem4  30120  strlem5  31495  hstrlem5  31503  abrexdomjm  31731  prct  31926  cyc3conja  32303  dvdschrmulg  32368  prmidl0  32557  dya2icoseg  33264  omssubadd  33287  omsmeas  33310  oddpwdc  33341  logdivsqrle  33650  faclim  34704  faclim2  34706  taupilem1  36190  mblfinlem3  36515  mblfinlem4  36516  ibladdnclem  36532  iblmulc2nc  36541  abrexdom  36586  dalem3  38523  dalem8  38529  dalem25  38557  dalem27  38558  dalem38  38569  dalem44  38575  dalem54  38585  lhpat3  38905  4atexlemunv  38925  4atexlemtlw  38926  4atexlemc  38928  4atexlemnclw  38929  4atexlemex2  38930  4atexlemcnd  38931  cdleme0b  39071  cdleme0c  39072  cdleme0fN  39077  cdlemeulpq  39079  cdleme01N  39080  cdleme0ex1N  39082  cdleme2  39087  cdleme3b  39088  cdleme3c  39089  cdleme3g  39093  cdleme3h  39094  cdleme4a  39098  cdleme7aa  39101  cdleme7c  39104  cdleme7d  39105  cdleme7e  39106  cdleme9  39112  cdleme11fN  39123  cdleme11k  39127  cdleme15d  39136  cdlemednpq  39158  cdleme19c  39164  cdleme20aN  39168  cdleme20e  39172  cdleme21c  39186  cdleme21ct  39188  cdleme22e  39203  cdleme22eALTN  39204  cdleme22f  39205  cdleme23a  39208  cdleme28a  39229  cdleme35f  39313  cdlemeg46frv  39384  cdlemeg46rgv  39387  cdlemeg46req  39388  cdlemg2fv2  39459  cdlemg2m  39463  cdlemg6c  39479  cdlemg31a  39556  cdlemg31b  39557  cdlemk10  39702  cdlemk37  39773  dia2dimlem1  39923  dihjatcclem4  40280  metakunt30  41002  3cubeslem1  41407  irrapxlem3  41547  pell14qrgapw  41599  dgrsub2  41862  radcnvrat  43058  ressiooinf  44256  fmul01  44282  fmul01lt1lem1  44286  fmul01lt1lem2  44287  sumnnodd  44332  climlimsupcex  44471  cnrefiisplem  44531  stoweidlem1  44703  stoweidlem5  44707  stoweidlem7  44709  dirkercncflem1  44805  dirkercncflem4  44808  fourierdlem30  44839  fourierdlem42  44851  fourierdlem48  44856  fourierdlem62  44870  fourierdlem63  44871  fourierdlem68  44876  fourierdlem79  44887  sqwvfoura  44930  etransclem32  44968  hoidmvlelem2  45298  iunhoiioolem  45377  vonioolem1  45382  pimdecfgtioo  45419  pimincfltioo  45420  smfmullem1  45493  fmtnoge3  46184  fmtnoprmfac2lem1  46220  sfprmdvdsmersenne  46257  lighneallem2  46260  lighneallem4a  46262  proththdlem  46267  stgoldbwt  46430  sgoldbeven3prm  46437  mogoldbb  46439  evengpop3  46452  bgoldbtbndlem2  46460  bgoldbtbndlem3  46461  lindslinindimp2lem3  47094  fllogbd  47199  nnolog2flm1  47229