Theorem eqbrtrid 5130

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096

This theorem is referenced by:  map1  8972  xp1en  8987  map2xp  9071  rex2dom  9152  sucxpdom  9160  sniffsupp  9309  wdomima2g  9497  endjudisj  10082  dju1dif  10086  mapdjuen  10094  djuxpdom  10099  djufi  10100  pwsdompw  10116  infunsdom1  10125  infunsdom  10126  infxp  10127  ackbij1lem5  10136  hsmexlem4  10342  imadomg  10447  unidom  10456  unictb  10488  pwxpndom2  10578  pwdjundom  10580  distrnq  10874  nnne0  12180  supxrmnf  13237  xov1plusxeqvd  13419  quoremz  13777  quoremnn0ALT  13779  intfrac2  13780  m1modge3gt1  13843  bernneq2  14155  faclbnd4lem1  14218  01sqrexlem4  15170  reccn2  15522  caucvg  15604  o1fsum  15738  infcvgaux2i  15783  eirrlem  16131  rpnnen2lem12  16152  ruclem12  16168  nno  16311  divalglem5  16326  bitsfzolem  16363  bitsinv1lem  16370  bezoutlem3  16470  lcmfunsnlem  16570  coprmproddvds  16592  oddprmge3  16629  ge2nprmge4  16630  sqnprm  16631  prmreclem6  16851  4sqlem6  16873  4sqlem13  16887  4sqlem16  16890  4sqlem17  16891  2expltfac  17022  odcau  19501  sylow3  19530  efginvrel2  19624  lt6abl  19792  ablfac1lem  19967  gzrngunitlem  21357  zringlpirlem3  21389  dvdschrmulg  21453  znfld  21485  evlslem2  22002  chfacffsupp  22759  cpmidpmatlem3  22775  cctop  22909  csdfil  23797  xpsdsval  24285  nrginvrcnlem  24595  icccmplem2  24728  reconnlem2  24732  iscmet3lem3  25206  minveclem2  25342  minveclem4  25348  ivthlem2  25369  ivthlem3  25370  ovolunlem1a  25413  ovolfiniun  25418  ovoliunlem3  25421  ovoliun  25422  ovolicc2lem4  25437  unmbl  25454  ioombl1lem4  25478  itg2mono  25670  ibladdlem  25737  iblabsr  25747  iblmulc2  25748  bddiblnc  25759  dvferm1lem  25904  dvferm2lem  25906  lhop1lem  25934  dvcvx  25941  ftc1a  25960  plyeq0lem  26131  aannenlem3  26254  geolim3  26263  psercnlem1  26351  pserdvlem2  26354  reeff1olem  26372  pilem2  26378  pilem3  26379  cosq14gt0  26435  cosq14ge0  26436  cosne0  26454  recosf1o  26460  resinf1o  26461  argregt0  26535  logcnlem3  26569  logcnlem4  26570  logf1o2  26575  cxpcn3lem  26673  ang180lem2  26736  acosbnd  26826  atanbndlem  26851  leibpi  26868  cxp2lim  26903  emcllem2  26923  ftalem5  27003  basellem9  27015  vmage0  27047  chpge0  27052  chtub  27139  mersenne  27154  bposlem2  27212  bposlem5  27215  bposlem6  27216  bposlem9  27219  gausslemma2dlem0c  27285  gausslemma2dlem0e  27287  lgseisenlem1  27302  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  chebbnd1lem1  27396  chebbnd1lem2  27397  chebbnd1lem3  27398  mulog2sumlem2  27462  pntpbnd1a  27512  pntibndlem1  27516  pntibndlem3  27519  pntlemc  27522  ostth2  27564  ostth3  27565  absmuls  28169  pthdlem1  29729  numclwlk1lem2  30332  smcnlem  30659  minvecolem2  30837  minvecolem4  30842  strlem5  32217  hstrlem5  32225  abrexdomjm  32469  prct  32671  cyc3conja  33112  elrgspnlem2  33196  prmidl0  33400  fldextrspunlsplem  33647  constrext2chnlem  33719  dya2icoseg  34247  omssubadd  34270  omsmeas  34293  oddpwdc  34324  logdivsqrle  34620  faclim  35721  faclim2  35723  taupilem1  37297  mblfinlem3  37641  mblfinlem4  37642  ibladdnclem  37658  iblmulc2nc  37667  abrexdom  37712  dalem3  39646  dalem8  39652  dalem25  39680  dalem27  39681  dalem38  39692  dalem44  39698  dalem54  39708  lhpat3  40028  4atexlemunv  40048  4atexlemtlw  40049  4atexlemc  40051  4atexlemnclw  40052  4atexlemex2  40053  4atexlemcnd  40054  cdleme0b  40194  cdleme0c  40195  cdleme0fN  40200  cdlemeulpq  40202  cdleme01N  40203  cdleme0ex1N  40205  cdleme2  40210  cdleme3b  40211  cdleme3c  40212  cdleme3g  40216  cdleme3h  40217  cdleme4a  40221  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme9  40235  cdleme11fN  40246  cdleme11k  40250  cdleme15d  40259  cdlemednpq  40281  cdleme19c  40287  cdleme20aN  40291  cdleme20e  40295  cdleme21c  40309  cdleme21ct  40311  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme23a  40331  cdleme28a  40352  cdleme35f  40436  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg6c  40602  cdlemg31a  40679  cdlemg31b  40680  cdlemk10  40825  cdlemk37  40896  dia2dimlem1  41046  dihjatcclem4  41403  imadomfi  41978  aks5lem1  42162  3cubeslem1  42660  irrapxlem3  42800  pell14qrgapw  42852  dgrsub2  43111  radcnvrat  44290  ressiooinf  45542  fmul01  45565  fmul01lt1lem1  45569  fmul01lt1lem2  45570  sumnnodd  45615  climlimsupcex  45754  cnrefiisplem  45814  stoweidlem1  45986  stoweidlem5  45990  stoweidlem7  45992  dirkercncflem1  46088  dirkercncflem4  46091  fourierdlem30  46122  fourierdlem42  46134  fourierdlem48  46139  fourierdlem62  46153  fourierdlem63  46154  fourierdlem68  46159  fourierdlem79  46170  sqwvfoura  46213  etransclem32  46251  hoidmvlelem2  46581  iunhoiioolem  46660  vonioolem1  46665  pimdecfgtioo  46702  pimincfltioo  46703  smfmullem1  46776  2ltceilhalf  47316  rehalfge1  47323  m1modnep2mod  47340  difmodm1lt  47347  fmtnoge3  47518  fmtnoprmfac2lem1  47554  sfprmdvdsmersenne  47591  lighneallem2  47594  lighneallem4a  47596  proththdlem  47601  stgoldbwt  47764  sgoldbeven3prm  47771  mogoldbb  47773  evengpop3  47786  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  lindslinindimp2lem3  48449  fllogbd  48549  nnolog2flm1  48579