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

Syntax hints:   → wi 4   = wceq 1570   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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111

This theorem is referenced by:  map1  9038  xp1en  9052  map2xp  9136  rex2dom  9214  sucxpdom  9222  sniffsupp  9361  wdomima2g  9549  endjudisj  10153  dju1dif  10157  mapdjuen  10165  djuxpdom  10170  djufi  10171  pwsdompw  10187  infunsdom1  10196  infunsdom  10197  infxp  10198  ackbij1lem5  10207  hsmexlem4  10414  imadomg  10519  unidom  10528  unictb  10561  pwxpndom2  10651  pwdjundom  10653  distrnq  10947  nnne0  12271  supxrmnf  13344  xov1plusxeqvd  13526  quoremz  13890  quoremnn0ALT  13892  intfrac2  13893  m1modge3gt1  13956  bernneq2  14268  faclbnd4lem1  14331  01sqrexlem4  15298  reccn2  15650  caucvg  15732  o1fsum  15867  infcvgaux2i  15914  eirrlem  16261  rpnnen2lem12  16282  ruclem12  16298  nno  16441  divalglem5  16456  bitsfzolem  16493  bitsinv1lem  16500  bezoutlem3  16600  lcmfunsnlem  16700  coprmproddvds  16722  oddprmge3  16760  ge2nprmge4  16761  sqnprm  16762  prmreclem6  16982  4sqlem6  17004  4sqlem13  17018  4sqlem16  17021  4sqlem17  17022  2expltfac  17153  odcau  19675  sylow3  19704  efginvrel2  19798  lt6abl  19966  ablfac1lem  20141  prmidl0  21459  gzrngunitlem  21563  zringlpirlem3  21595  dvdschrmulg  21659  znfld  21691  evlslem2  22211  chfacffsupp  22994  cpmidpmatlem3  23010  cctop  23144  csdfil  24032  xpsdsval  24519  nrginvrcnlem  24829  icccmplem2  24962  reconnlem2  24966  iscmet3lem3  25430  minveclem2  25566  minveclem4  25572  ivthlem2  25592  ivthlem3  25593  ovolunlem1a  25636  ovolfiniun  25641  ovoliunlem3  25644  ovoliun  25645  ovolicc2lem4  25660  unmbl  25677  ioombl1lem4  25701  itg2mono  25893  ibladdlem  25960  iblabsr  25970  iblmulc2  25971  bddiblnc  25982  dvferm1lem  26124  dvferm2lem  26126  lhop1lem  26153  dvcvx  26160  ftc1a  26177  plyeq0lem  26348  aannenlem3  26474  geolim3  26483  psercnlem1  26569  pserdvlem2  26572  reeff1olem  26590  pilem2  26596  pilem3  26597  cosq14gt0  26656  cosq14ge0  26657  cosne0  26675  recosf1o  26681  resinf1o  26682  argregt0  26756  logcnlem3  26790  logcnlem4  26791  logf1o2  26796  cxpcn3lem  26893  ang180lem2  26956  acosbnd  27046  atanbndlem  27071  leibpi  27088  cxp2lim  27122  emcllem2  27142  ftalem5  27222  basellem9  27234  vmage0  27266  chpge0  27271  chtub  27357  mersenne  27372  bposlem2  27430  bposlem5  27433  bposlem6  27434  bposlem9  27437  gausslemma2dlem0c  27503  gausslemma2dlem0e  27505  lgseisenlem1  27520  lgsquadlem1  27525  lgsquadlem2  27526  lgsquadlem3  27527  chebbnd1lem1  27614  chebbnd1lem2  27615  chebbnd1lem3  27616  mulog2sumlem2  27680  pntpbnd1a  27730  pntibndlem1  27734  pntibndlem3  27737  pntlemc  27740  ostth2  27782  ostth3  27783  absmuls  28418  pthdlem1  30096  numclwlk1lem2  30702  smcnlem  31030  minvecolem2  31208  minvecolem4  31213  strlem5  32588  hstrlem5  32596  abrexdomjm  32834  prct  33039  cyc3conja  33458  elrgspnlem2  33544  mplvrpmga  33916  psrmonprod  33923  fldextrspunlsplem  34044  constrext2chnlem  34121  dya2icoseg  34648  omssubadd  34671  omsmeas  34694  oddpwdc  34725  logdivsqrle  35018  faclim  36219  faclim2  36221  taupilem1  37946  mblfinlem3  38291  mblfinlem4  38292  ibladdnclem  38308  iblmulc2nc  38317  abrexdom  38362  dalem3  40419  dalem8  40425  dalem25  40453  dalem27  40454  dalem38  40465  dalem44  40471  dalem54  40481  lhpat3  40801  4atexlemunv  40821  4atexlemtlw  40822  4atexlemc  40824  4atexlemnclw  40825  4atexlemex2  40826  4atexlemcnd  40827  cdleme0b  40967  cdleme0c  40968  cdleme0fN  40973  cdlemeulpq  40975  cdleme01N  40976  cdleme0ex1N  40978  cdleme2  40983  cdleme3b  40984  cdleme3c  40985  cdleme3g  40989  cdleme3h  40990  cdleme4a  40994  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme9  41008  cdleme11fN  41019  cdleme11k  41023  cdleme15d  41032  cdlemednpq  41054  cdleme19c  41060  cdleme20aN  41064  cdleme20e  41068  cdleme21c  41082  cdleme21ct  41084  cdleme22e  41099  cdleme22eALTN  41100  cdleme22f  41101  cdleme23a  41104  cdleme28a  41125  cdleme35f  41209  cdlemeg46frv  41280  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemg2fv2  41355  cdlemg2m  41359  cdlemg6c  41375  cdlemg31a  41452  cdlemg31b  41453  cdlemk10  41598  cdlemk37  41669  dia2dimlem1  41819  dihjatcclem4  42176  imadomfi  42750  aks5lem1  42934  3cubeslem1  43398  irrapxlem3  43534  pell14qrgapw  43586  dgrsub2  43845  radcnvrat  45007  ressiooinf  46256  fmul01  46279  fmul01lt1lem1  46283  fmul01lt1lem2  46284  sumnnodd  46329  climlimsupcex  46466  cnrefiisplem  46526  stoweidlem1  46698  stoweidlem5  46702  stoweidlem7  46704  dirkercncflem1  46800  dirkercncflem4  46803  fourierdlem30  46834  fourierdlem42  46846  fourierdlem48  46851  fourierdlem49  46852  fourierdlem62  46865  fourierdlem63  46866  fourierdlem68  46871  fourierdlem79  46882  sqwvfoura  46925  etransclem32  46963  hoidmvlelem2  47293  iunhoiioolem  47372  vonioolem1  47377  pimdecfgtioo  47414  pimincfltioo  47415  smfmullem1  47488  2ltceilhalf  48052  rehalfge1  48059  m1modnep2mod  48078  difmodm1lt  48085  2timesltsqm1  48099  fmtnoge3  48265  fmtnoprmfac2lem1  48301  sfprmdvdsmersenne  48338  lighneallem2  48341  lighneallem4a  48343  proththdlem  48348  nprmdvdsfacm1lem2  48356  stgoldbwt  48524  sgoldbeven3prm  48531  mogoldbb  48533  evengpop3  48546  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  lindslinindimp2lem3  49223  fllogbd  49323  nnolog2flm1  49353