Theorem eqbrtrid 5137

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 5136	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  map1  8988  xp1en  9004  map2xp  9088  rex2dom  9169  1sdomOLD  9172  sucxpdom  9178  sniffsupp  9327  wdomima2g  9515  endjudisj  10098  dju1dif  10102  mapdjuen  10110  djuxpdom  10115  djufi  10116  pwsdompw  10132  infunsdom1  10141  infunsdom  10142  infxp  10143  ackbij1lem5  10152  hsmexlem4  10358  imadomg  10463  unidom  10472  unictb  10504  pwxpndom2  10594  pwdjundom  10596  distrnq  10890  nnne0  12196  supxrmnf  13253  xov1plusxeqvd  13435  quoremz  13793  quoremnn0ALT  13795  intfrac2  13796  m1modge3gt1  13859  bernneq2  14171  faclbnd4lem1  14234  01sqrexlem4  15187  reccn2  15539  caucvg  15621  o1fsum  15755  infcvgaux2i  15800  eirrlem  16148  rpnnen2lem12  16169  ruclem12  16185  nno  16328  divalglem5  16343  bitsfzolem  16380  bitsinv1lem  16387  bezoutlem3  16487  lcmfunsnlem  16587  coprmproddvds  16609  oddprmge3  16646  ge2nprmge4  16647  sqnprm  16648  prmreclem6  16868  4sqlem6  16890  4sqlem13  16904  4sqlem16  16907  4sqlem17  16908  2expltfac  17039  odcau  19510  sylow3  19539  efginvrel2  19633  lt6abl  19801  ablfac1lem  19976  gzrngunitlem  21325  zringlpirlem3  21350  dvdschrmulg  21414  znfld  21446  evlslem2  21962  chfacffsupp  22719  cpmidpmatlem3  22735  cctop  22869  csdfil  23757  xpsdsval  24245  nrginvrcnlem  24555  icccmplem2  24688  reconnlem2  24692  iscmet3lem3  25166  minveclem2  25302  minveclem4  25308  ivthlem2  25329  ivthlem3  25330  ovolunlem1a  25373  ovolfiniun  25378  ovoliunlem3  25381  ovoliun  25382  ovolicc2lem4  25397  unmbl  25414  ioombl1lem4  25438  itg2mono  25630  ibladdlem  25697  iblabsr  25707  iblmulc2  25708  bddiblnc  25719  dvferm1lem  25864  dvferm2lem  25866  lhop1lem  25894  dvcvx  25901  ftc1a  25920  plyeq0lem  26091  aannenlem3  26214  geolim3  26223  psercnlem1  26311  pserdvlem2  26314  reeff1olem  26332  pilem2  26338  pilem3  26339  cosq14gt0  26395  cosq14ge0  26396  cosne0  26414  recosf1o  26420  resinf1o  26421  argregt0  26495  logcnlem3  26529  logcnlem4  26530  logf1o2  26535  cxpcn3lem  26633  ang180lem2  26696  acosbnd  26786  atanbndlem  26811  leibpi  26828  cxp2lim  26863  emcllem2  26883  ftalem5  26963  basellem9  26975  vmage0  27007  chpge0  27012  chtub  27099  mersenne  27114  bposlem2  27172  bposlem5  27175  bposlem6  27176  bposlem9  27179  gausslemma2dlem0c  27245  gausslemma2dlem0e  27247  lgseisenlem1  27262  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  chebbnd1lem1  27356  chebbnd1lem2  27357  chebbnd1lem3  27358  mulog2sumlem2  27422  pntpbnd1a  27472  pntibndlem1  27476  pntibndlem3  27479  pntlemc  27482  ostth2  27524  ostth3  27525  absmuls  28122  pthdlem1  29669  numclwlk1lem2  30272  smcnlem  30599  minvecolem2  30777  minvecolem4  30782  strlem5  32157  hstrlem5  32165  abrexdomjm  32409  prct  32611  cyc3conja  33087  elrgspnlem2  33167  prmidl0  33394  fldextrspunlsplem  33641  constrext2chnlem  33713  dya2icoseg  34241  omssubadd  34264  omsmeas  34287  oddpwdc  34318  logdivsqrle  34614  faclim  35706  faclim2  35708  taupilem1  37282  mblfinlem3  37626  mblfinlem4  37627  ibladdnclem  37643  iblmulc2nc  37652  abrexdom  37697  dalem3  39631  dalem8  39637  dalem25  39665  dalem27  39666  dalem38  39677  dalem44  39683  dalem54  39693  lhpat3  40013  4atexlemunv  40033  4atexlemtlw  40034  4atexlemc  40036  4atexlemnclw  40037  4atexlemex2  40038  4atexlemcnd  40039  cdleme0b  40179  cdleme0c  40180  cdleme0fN  40185  cdlemeulpq  40187  cdleme01N  40188  cdleme0ex1N  40190  cdleme2  40195  cdleme3b  40196  cdleme3c  40197  cdleme3g  40201  cdleme3h  40202  cdleme4a  40206  cdleme7aa  40209  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme9  40220  cdleme11fN  40231  cdleme11k  40235  cdleme15d  40244  cdlemednpq  40266  cdleme19c  40272  cdleme20aN  40276  cdleme20e  40280  cdleme21c  40294  cdleme21ct  40296  cdleme22e  40311  cdleme22eALTN  40312  cdleme22f  40313  cdleme23a  40316  cdleme28a  40337  cdleme35f  40421  cdlemeg46frv  40492  cdlemeg46rgv  40495  cdlemeg46req  40496  cdlemg2fv2  40567  cdlemg2m  40571  cdlemg6c  40587  cdlemg31a  40664  cdlemg31b  40665  cdlemk10  40810  cdlemk37  40881  dia2dimlem1  41031  dihjatcclem4  41388  imadomfi  41963  aks5lem1  42147  3cubeslem1  42645  irrapxlem3  42785  pell14qrgapw  42837  dgrsub2  43097  radcnvrat  44276  ressiooinf  45528  fmul01  45551  fmul01lt1lem1  45555  fmul01lt1lem2  45556  sumnnodd  45601  climlimsupcex  45740  cnrefiisplem  45800  stoweidlem1  45972  stoweidlem5  45976  stoweidlem7  45978  dirkercncflem1  46074  dirkercncflem4  46077  fourierdlem30  46108  fourierdlem42  46120  fourierdlem48  46125  fourierdlem62  46139  fourierdlem63  46140  fourierdlem68  46145  fourierdlem79  46156  sqwvfoura  46199  etransclem32  46237  hoidmvlelem2  46567  iunhoiioolem  46646  vonioolem1  46651  pimdecfgtioo  46688  pimincfltioo  46689  smfmullem1  46762  2ltceilhalf  47302  rehalfge1  47309  m1modnep2mod  47326  difmodm1lt  47333  fmtnoge3  47504  fmtnoprmfac2lem1  47540  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem4a  47582  proththdlem  47587  stgoldbwt  47750  sgoldbeven3prm  47757  mogoldbb  47759  evengpop3  47772  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  lindslinindimp2lem3  48422  fllogbd  48522  nnolog2flm1  48552