Theorem eqbrtrid 5147

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  map1  9033  xp1en  9047  map2xp  9131  rex2dom  9209  sucxpdom  9217  sniffsupp  9356  wdomima2g  9544  endjudisj  10148  dju1dif  10152  mapdjuen  10160  djuxpdom  10165  djufi  10166  pwsdompw  10182  infunsdom1  10191  infunsdom  10192  infxp  10193  ackbij1lem5  10202  hsmexlem4  10409  imadomg  10514  unidom  10523  unictb  10556  pwxpndom2  10646  pwdjundom  10648  distrnq  10942  nnne0  12266  supxrmnf  13339  xov1plusxeqvd  13521  quoremz  13884  quoremnn0ALT  13886  intfrac2  13887  m1modge3gt1  13950  bernneq2  14262  faclbnd4lem1  14325  01sqrexlem4  15292  reccn2  15644  caucvg  15726  o1fsum  15861  infcvgaux2i  15908  eirrlem  16256  rpnnen2lem12  16277  ruclem12  16293  nno  16436  divalglem5  16451  bitsfzolem  16488  bitsinv1lem  16495  bezoutlem3  16595  lcmfunsnlem  16695  coprmproddvds  16717  oddprmge3  16755  ge2nprmge4  16756  sqnprm  16757  prmreclem6  16977  4sqlem6  16999  4sqlem13  17013  4sqlem16  17016  4sqlem17  17017  2expltfac  17148  odcau  19670  sylow3  19699  efginvrel2  19793  lt6abl  19961  ablfac1lem  20136  prmidl0  21443  gzrngunitlem  21547  zringlpirlem3  21579  dvdschrmulg  21643  znfld  21675  evlslem2  22195  chfacffsupp  22978  cpmidpmatlem3  22994  cctop  23128  csdfil  24016  xpsdsval  24503  nrginvrcnlem  24813  icccmplem2  24946  reconnlem2  24950  iscmet3lem3  25414  minveclem2  25550  minveclem4  25556  ivthlem2  25576  ivthlem3  25577  ovolunlem1a  25620  ovolfiniun  25625  ovoliunlem3  25628  ovoliun  25629  ovolicc2lem4  25644  unmbl  25661  ioombl1lem4  25685  itg2mono  25877  ibladdlem  25944  iblabsr  25954  iblmulc2  25955  bddiblnc  25966  dvferm1lem  26108  dvferm2lem  26110  lhop1lem  26137  dvcvx  26144  ftc1a  26161  plyeq0lem  26332  aannenlem3  26456  geolim3  26465  psercnlem1  26550  pserdvlem2  26553  reeff1olem  26571  pilem2  26577  pilem3  26578  cosq14gt0  26637  cosq14ge0  26638  cosne0  26656  recosf1o  26662  resinf1o  26663  argregt0  26737  logcnlem3  26771  logcnlem4  26772  logf1o2  26777  cxpcn3lem  26874  ang180lem2  26937  acosbnd  27027  atanbndlem  27052  leibpi  27069  cxp2lim  27103  emcllem2  27123  ftalem5  27203  basellem9  27215  vmage0  27247  chpge0  27252  chtub  27338  mersenne  27353  bposlem2  27411  bposlem5  27414  bposlem6  27415  bposlem9  27418  gausslemma2dlem0c  27484  gausslemma2dlem0e  27486  lgseisenlem1  27501  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  chebbnd1lem1  27595  chebbnd1lem2  27596  chebbnd1lem3  27597  mulog2sumlem2  27661  pntpbnd1a  27711  pntibndlem1  27715  pntibndlem3  27718  pntlemc  27721  ostth2  27763  ostth3  27764  absmuls  28399  pthdlem1  30052  numclwlk1lem2  30658  smcnlem  30986  minvecolem2  31164  minvecolem4  31169  strlem5  32544  hstrlem5  32552  abrexdomjm  32790  prct  32995  cyc3conja  33414  elrgspnlem2  33500  mplvrpmga  33876  psrmonprod  33883  fldextrspunlsplem  34004  constrext2chnlem  34081  dya2icoseg  34608  omssubadd  34631  omsmeas  34654  oddpwdc  34685  logdivsqrle  34978  faclim  36133  faclim2  36135  taupilem1  37848  mblfinlem3  38193  mblfinlem4  38194  ibladdnclem  38210  iblmulc2nc  38219  abrexdom  38264  dalem3  40323  dalem8  40329  dalem25  40357  dalem27  40358  dalem38  40369  dalem44  40375  dalem54  40385  lhpat3  40705  4atexlemunv  40725  4atexlemtlw  40726  4atexlemc  40728  4atexlemnclw  40729  4atexlemex2  40730  4atexlemcnd  40731  cdleme0b  40871  cdleme0c  40872  cdleme0fN  40877  cdlemeulpq  40879  cdleme01N  40880  cdleme0ex1N  40882  cdleme2  40887  cdleme3b  40888  cdleme3c  40889  cdleme3g  40893  cdleme3h  40894  cdleme4a  40898  cdleme7aa  40901  cdleme7c  40904  cdleme7d  40905  cdleme7e  40906  cdleme9  40912  cdleme11fN  40923  cdleme11k  40927  cdleme15d  40936  cdlemednpq  40958  cdleme19c  40964  cdleme20aN  40968  cdleme20e  40972  cdleme21c  40986  cdleme21ct  40988  cdleme22e  41003  cdleme22eALTN  41004  cdleme22f  41005  cdleme23a  41008  cdleme28a  41029  cdleme35f  41113  cdlemeg46frv  41184  cdlemeg46rgv  41187  cdlemeg46req  41188  cdlemg2fv2  41259  cdlemg2m  41263  cdlemg6c  41279  cdlemg31a  41356  cdlemg31b  41357  cdlemk10  41502  cdlemk37  41573  dia2dimlem1  41723  dihjatcclem4  42080  imadomfi  42654  aks5lem1  42838  3cubeslem1  43300  irrapxlem3  43436  pell14qrgapw  43488  dgrsub2  43747  radcnvrat  44909  ressiooinf  46158  fmul01  46181  fmul01lt1lem1  46185  fmul01lt1lem2  46186  sumnnodd  46231  climlimsupcex  46368  cnrefiisplem  46428  stoweidlem1  46600  stoweidlem5  46604  stoweidlem7  46606  dirkercncflem1  46702  dirkercncflem4  46705  fourierdlem30  46736  fourierdlem42  46748  fourierdlem48  46753  fourierdlem49  46754  fourierdlem62  46767  fourierdlem63  46768  fourierdlem68  46773  fourierdlem79  46784  sqwvfoura  46827  etransclem32  46865  hoidmvlelem2  47195  iunhoiioolem  47274  vonioolem1  47279  pimdecfgtioo  47316  pimincfltioo  47317  smfmullem1  47390  2ltceilhalf  47951  rehalfge1  47958  m1modnep2mod  47977  difmodm1lt  47984  2timesltsqm1  47998  fmtnoge3  48164  fmtnoprmfac2lem1  48200  sfprmdvdsmersenne  48237  lighneallem2  48240  lighneallem4a  48242  proththdlem  48247  nprmdvdsfacm1lem2  48255  stgoldbwt  48423  sgoldbeven3prm  48430  mogoldbb  48432  evengpop3  48445  bgoldbtbndlem2  48453  bgoldbtbndlem3  48454  lindslinindimp2lem3  49118  fllogbd  49218  nnolog2flm1  49248