Theorem eqbrtrid 5132

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

Syntax hints:   → wi 4   = wceq 1559   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  map1  9014  xp1en  9028  map2xp  9112  rex2dom  9190  sucxpdom  9198  sniffsupp  9339  wdomima2g  9527  endjudisj  10118  dju1dif  10122  mapdjuen  10130  djuxpdom  10135  djufi  10136  pwsdompw  10152  infunsdom1  10161  infunsdom  10162  infxp  10163  ackbij1lem5  10172  hsmexlem4  10379  imadomg  10484  unidom  10493  unictb  10526  pwxpndom2  10616  pwdjundom  10618  distrnq  10912  nnne0  12240  supxrmnf  13313  xov1plusxeqvd  13495  quoremz  13858  quoremnn0ALT  13860  intfrac2  13861  m1modge3gt1  13924  bernneq2  14236  faclbnd4lem1  14299  01sqrexlem4  15262  reccn2  15614  caucvg  15696  o1fsum  15831  infcvgaux2i  15878  eirrlem  16226  rpnnen2lem12  16247  ruclem12  16263  nno  16406  divalglem5  16421  bitsfzolem  16458  bitsinv1lem  16465  bezoutlem3  16565  lcmfunsnlem  16665  coprmproddvds  16687  oddprmge3  16725  ge2nprmge4  16726  sqnprm  16727  prmreclem6  16947  4sqlem6  16969  4sqlem13  16983  4sqlem16  16986  4sqlem17  16987  2expltfac  17118  odcau  19634  sylow3  19663  efginvrel2  19757  lt6abl  19925  ablfac1lem  20100  gzrngunitlem  21471  zringlpirlem3  21503  dvdschrmulg  21567  znfld  21599  evlslem2  22119  chfacffsupp  22903  cpmidpmatlem3  22919  cctop  23053  csdfil  23941  xpsdsval  24428  nrginvrcnlem  24738  icccmplem2  24871  reconnlem2  24875  iscmet3lem3  25339  minveclem2  25475  minveclem4  25481  ivthlem2  25501  ivthlem3  25502  ovolunlem1a  25545  ovolfiniun  25550  ovoliunlem3  25553  ovoliun  25554  ovolicc2lem4  25569  unmbl  25586  ioombl1lem4  25610  itg2mono  25802  ibladdlem  25869  iblabsr  25879  iblmulc2  25880  bddiblnc  25891  dvferm1lem  26033  dvferm2lem  26035  lhop1lem  26062  dvcvx  26069  ftc1a  26086  plyeq0lem  26257  aannenlem3  26381  geolim3  26390  psercnlem1  26475  pserdvlem2  26478  reeff1olem  26496  pilem2  26502  pilem3  26503  cosq14gt0  26562  cosq14ge0  26563  cosne0  26581  recosf1o  26587  resinf1o  26588  argregt0  26662  logcnlem3  26696  logcnlem4  26697  logf1o2  26702  cxpcn3lem  26799  ang180lem2  26862  acosbnd  26952  atanbndlem  26977  leibpi  26994  cxp2lim  27028  emcllem2  27048  ftalem5  27128  basellem9  27140  vmage0  27172  chpge0  27177  chtub  27263  mersenne  27278  bposlem2  27336  bposlem5  27339  bposlem6  27340  bposlem9  27343  gausslemma2dlem0c  27409  gausslemma2dlem0e  27411  lgseisenlem1  27426  lgsquadlem1  27431  lgsquadlem2  27432  lgsquadlem3  27433  chebbnd1lem1  27520  chebbnd1lem2  27521  chebbnd1lem3  27522  mulog2sumlem2  27586  pntpbnd1a  27636  pntibndlem1  27640  pntibndlem3  27643  pntlemc  27646  ostth2  27688  ostth3  27689  absmuls  28324  pthdlem1  29922  numclwlk1lem2  30528  smcnlem  30856  minvecolem2  31034  minvecolem4  31039  strlem5  32414  hstrlem5  32422  abrexdomjm  32665  prct  32875  cyc3conja  33297  elrgspnlem2  33384  prmidl0  33597  mplvrpmga  33802  psrmonprod  33809  fldextrspunlsplem  33930  constrext2chnlem  34007  dya2icoseg  34534  omssubadd  34557  omsmeas  34580  oddpwdc  34611  logdivsqrle  34904  faclim  36056  faclim2  36058  taupilem1  37773  mblfinlem3  38118  mblfinlem4  38119  ibladdnclem  38135  iblmulc2nc  38144  abrexdom  38189  dalem3  40248  dalem8  40254  dalem25  40282  dalem27  40283  dalem38  40294  dalem44  40300  dalem54  40310  lhpat3  40630  4atexlemunv  40650  4atexlemtlw  40651  4atexlemc  40653  4atexlemnclw  40654  4atexlemex2  40655  4atexlemcnd  40656  cdleme0b  40796  cdleme0c  40797  cdleme0fN  40802  cdlemeulpq  40804  cdleme01N  40805  cdleme0ex1N  40807  cdleme2  40812  cdleme3b  40813  cdleme3c  40814  cdleme3g  40818  cdleme3h  40819  cdleme4a  40823  cdleme7aa  40826  cdleme7c  40829  cdleme7d  40830  cdleme7e  40831  cdleme9  40837  cdleme11fN  40848  cdleme11k  40852  cdleme15d  40861  cdlemednpq  40883  cdleme19c  40889  cdleme20aN  40893  cdleme20e  40897  cdleme21c  40911  cdleme21ct  40913  cdleme22e  40928  cdleme22eALTN  40929  cdleme22f  40930  cdleme23a  40933  cdleme28a  40954  cdleme35f  41038  cdlemeg46frv  41109  cdlemeg46rgv  41112  cdlemeg46req  41113  cdlemg2fv2  41184  cdlemg2m  41188  cdlemg6c  41204  cdlemg31a  41281  cdlemg31b  41282  cdlemk10  41427  cdlemk37  41498  dia2dimlem1  41648  dihjatcclem4  42005  imadomfi  42579  aks5lem1  42763  3cubeslem1  43225  irrapxlem3  43361  pell14qrgapw  43413  dgrsub2  43672  radcnvrat  44850  ressiooinf  46093  fmul01  46116  fmul01lt1lem1  46120  fmul01lt1lem2  46121  sumnnodd  46166  climlimsupcex  46303  cnrefiisplem  46363  stoweidlem1  46535  stoweidlem5  46539  stoweidlem7  46541  dirkercncflem1  46637  dirkercncflem4  46640  fourierdlem30  46671  fourierdlem42  46683  fourierdlem48  46688  fourierdlem49  46689  fourierdlem62  46702  fourierdlem63  46703  fourierdlem68  46708  fourierdlem79  46719  sqwvfoura  46762  etransclem32  46800  hoidmvlelem2  47130  iunhoiioolem  47209  vonioolem1  47214  pimdecfgtioo  47251  pimincfltioo  47252  smfmullem1  47325  2ltceilhalf  47886  rehalfge1  47893  m1modnep2mod  47912  difmodm1lt  47919  2timesltsqm1  47933  fmtnoge3  48099  fmtnoprmfac2lem1  48135  sfprmdvdsmersenne  48172  lighneallem2  48175  lighneallem4a  48177  proththdlem  48182  nprmdvdsfacm1lem2  48190  stgoldbwt  48358  sgoldbeven3prm  48365  mogoldbb  48367  evengpop3  48380  bgoldbtbndlem2  48388  bgoldbtbndlem3  48389  lindslinindimp2lem3  49042  fllogbd  49142  nnolog2flm1  49172