Theorem eqbrtrid 5184

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

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

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  map1  9040  xp1en  9057  map2xp  9147  rex2dom  9246  1sdomOLD  9249  sucxpdom  9255  sniffsupp  9395  wdomima2g  9581  endjudisj  10163  dju1dif  10167  mapdjuen  10175  djuxpdom  10180  djufi  10181  pwsdompw  10199  infunsdom1  10208  infunsdom  10209  infxp  10210  ackbij1lem5  10219  hsmexlem4  10424  imadomg  10529  unidom  10538  unictb  10570  pwxpndom2  10660  pwdjundom  10662  distrnq  10956  nnne0  12246  supxrmnf  13296  xov1plusxeqvd  13475  quoremz  13820  quoremnn0ALT  13822  intfrac2  13823  m1modge3gt1  13883  bernneq2  14193  faclbnd4lem1  14253  01sqrexlem4  15192  reccn2  15541  caucvg  15625  o1fsum  15759  infcvgaux2i  15804  eirrlem  16147  rpnnen2lem12  16168  ruclem12  16184  nno  16325  divalglem5  16340  bitsfzolem  16375  bitsinv1lem  16382  bezoutlem3  16483  lcmfunsnlem  16578  coprmproddvds  16600  oddprmge3  16637  ge2nprmge4  16638  sqnprm  16639  prmreclem6  16854  4sqlem6  16876  4sqlem13  16890  4sqlem16  16893  4sqlem17  16894  2expltfac  17026  odcau  19472  sylow3  19501  efginvrel2  19595  lt6abl  19763  ablfac1lem  19938  gzrngunitlem  21010  zringlpirlem3  21034  znfld  21116  evlslem2  21642  chfacffsupp  22358  cpmidpmatlem3  22374  cctop  22509  csdfil  23398  xpsdsval  23887  nrginvrcnlem  24208  icccmplem2  24339  reconnlem2  24343  iscmet3lem3  24807  minveclem2  24943  minveclem4  24949  ivthlem2  24969  ivthlem3  24970  ovolunlem1a  25013  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovolicc2lem4  25037  unmbl  25054  ioombl1lem4  25078  itg2mono  25271  ibladdlem  25337  iblabsr  25347  iblmulc2  25348  bddiblnc  25359  dvferm1lem  25501  dvferm2lem  25503  lhop1lem  25530  dvcvx  25537  ftc1a  25554  plyeq0lem  25724  aannenlem3  25843  geolim3  25852  psercnlem1  25937  pserdvlem2  25940  reeff1olem  25958  pilem2  25964  pilem3  25965  cosq14gt0  26020  cosq14ge0  26021  cosne0  26038  recosf1o  26044  resinf1o  26045  argregt0  26118  logcnlem3  26152  logcnlem4  26153  logf1o2  26158  cxpcn3lem  26255  ang180lem2  26315  acosbnd  26405  atanbndlem  26430  leibpi  26447  cxp2lim  26481  emcllem2  26501  ftalem5  26581  basellem9  26593  vmage0  26625  chpge0  26630  chtub  26715  mersenne  26730  bposlem2  26788  bposlem5  26791  bposlem6  26792  bposlem9  26795  gausslemma2dlem0c  26861  gausslemma2dlem0e  26863  lgseisenlem1  26878  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  chebbnd1lem1  26972  chebbnd1lem2  26973  chebbnd1lem3  26974  mulog2sumlem2  27038  pntpbnd1a  27088  pntibndlem1  27092  pntibndlem3  27095  pntlemc  27098  ostth2  27140  ostth3  27141  pthdlem1  29023  numclwlk1lem2  29623  smcnlem  29950  minvecolem2  30128  minvecolem4  30133  strlem5  31508  hstrlem5  31516  abrexdomjm  31744  prct  31939  cyc3conja  32316  dvdschrmulg  32380  prmidl0  32569  dya2icoseg  33276  omssubadd  33299  omsmeas  33322  oddpwdc  33353  logdivsqrle  33662  faclim  34716  faclim2  34718  taupilem1  36202  mblfinlem3  36527  mblfinlem4  36528  ibladdnclem  36544  iblmulc2nc  36553  abrexdom  36598  dalem3  38535  dalem8  38541  dalem25  38569  dalem27  38570  dalem38  38581  dalem44  38587  dalem54  38597  lhpat3  38917  4atexlemunv  38937  4atexlemtlw  38938  4atexlemc  38940  4atexlemnclw  38941  4atexlemex2  38942  4atexlemcnd  38943  cdleme0b  39083  cdleme0c  39084  cdleme0fN  39089  cdlemeulpq  39091  cdleme01N  39092  cdleme0ex1N  39094  cdleme2  39099  cdleme3b  39100  cdleme3c  39101  cdleme3g  39105  cdleme3h  39106  cdleme4a  39110  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme9  39124  cdleme11fN  39135  cdleme11k  39139  cdleme15d  39148  cdlemednpq  39170  cdleme19c  39176  cdleme20aN  39180  cdleme20e  39184  cdleme21c  39198  cdleme21ct  39200  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme23a  39220  cdleme28a  39241  cdleme35f  39325  cdlemeg46frv  39396  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemg2fv2  39471  cdlemg2m  39475  cdlemg6c  39491  cdlemg31a  39568  cdlemg31b  39569  cdlemk10  39714  cdlemk37  39785  dia2dimlem1  39935  dihjatcclem4  40292  metakunt30  41014  3cubeslem1  41422  irrapxlem3  41562  pell14qrgapw  41614  dgrsub2  41877  radcnvrat  43073  ressiooinf  44270  fmul01  44296  fmul01lt1lem1  44300  fmul01lt1lem2  44301  sumnnodd  44346  climlimsupcex  44485  cnrefiisplem  44545  stoweidlem1  44717  stoweidlem5  44721  stoweidlem7  44723  dirkercncflem1  44819  dirkercncflem4  44822  fourierdlem30  44853  fourierdlem42  44865  fourierdlem48  44870  fourierdlem62  44884  fourierdlem63  44885  fourierdlem68  44890  fourierdlem79  44901  sqwvfoura  44944  etransclem32  44982  hoidmvlelem2  45312  iunhoiioolem  45391  vonioolem1  45396  pimdecfgtioo  45433  pimincfltioo  45434  smfmullem1  45507  fmtnoge3  46198  fmtnoprmfac2lem1  46234  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem4a  46276  proththdlem  46281  stgoldbwt  46444  sgoldbeven3prm  46451  mogoldbb  46453  evengpop3  46466  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  lindslinindimp2lem3  47141  fllogbd  47246  nnolog2flm1  47276