Theorem eqbrtrid 5148

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  map1  9040  xp1en  9054  map2xp  9138  rex2dom  9216  sucxpdom  9224  sniffsupp  9363  wdomima2g  9551  endjudisj  10164  dju1dif  10168  mapdjuen  10176  djuxpdom  10181  djufi  10182  pwsdompw  10198  infunsdom1  10207  infunsdom  10208  infxp  10209  ackbij1lem5  10218  hsmexlem4  10424  imadomg  10529  unidom  10538  unictb  10571  pwxpndom2  10661  pwdjundom  10663  distrnq  10957  nnne0  12281  supxrmnf  13354  xov1plusxeqvd  13536  quoremz  13901  quoremnn0ALT  13903  intfrac2  13904  m1modge3gt1  13967  bernneq2  14279  faclbnd4lem1  14342  01sqrexlem4  15315  reccn2  15667  caucvg  15749  o1fsum  15883  infcvgaux2i  15930  eirrlem  16277  rpnnen2lem12  16298  ruclem12  16314  nno  16457  divalglem5  16472  bitsfzolem  16509  bitsinv1lem  16516  bezoutlem3  16616  lcmfunsnlem  16716  coprmproddvds  16738  oddprmge3  16776  ge2nprmge4  16777  sqnprm  16778  prmreclem6  16998  4sqlem6  17020  4sqlem13  17034  4sqlem16  17037  4sqlem17  17038  2expltfac  17169  odcau  19697  sylow3  19726  efginvrel2  19820  lt6abl  19988  ablfac1lem  20163  prmidl0  21507  gzrngunitlem  21611  zringlpirlem3  21643  dvdschrmulg  21707  znfld  21739  evlslem2  22259  chfacffsupp  23042  cpmidpmatlem3  23058  cctop  23192  csdfil  24080  xpsdsval  24567  nrginvrcnlem  24877  icccmplem2  25010  reconnlem2  25014  iscmet3lem3  25478  minveclem2  25614  minveclem4  25620  ivthlem2  25640  ivthlem3  25641  ovolunlem1a  25684  ovolfiniun  25689  ovoliunlem3  25692  ovoliun  25693  ovolicc2lem4  25708  unmbl  25725  ioombl1lem4  25749  itg2mono  25941  ibladdlem  26008  iblabsr  26018  iblmulc2  26019  bddiblnc  26030  dvferm1lem  26172  dvferm2lem  26174  lhop1lem  26201  dvcvx  26208  ftc1a  26225  plyeq0lem  26396  aannenlem3  26522  geolim3  26531  psercnlem1  26617  pserdvlem2  26620  reeff1olem  26638  pilem2  26644  pilem3  26645  cosq14gt0  26704  cosq14ge0  26705  cosne0  26723  recosf1o  26729  resinf1o  26730  argregt0  26804  logcnlem3  26838  logcnlem4  26839  logf1o2  26844  cxpcn3lem  26941  ang180lem2  27004  acosbnd  27094  atanbndlem  27119  leibpi  27136  cxp2lim  27170  emcllem2  27190  ftalem5  27270  basellem9  27282  vmage0  27314  chpge0  27319  chtub  27405  mersenne  27420  bposlem2  27478  bposlem5  27481  bposlem6  27482  bposlem9  27485  gausslemma2dlem0c  27551  gausslemma2dlem0e  27553  lgseisenlem1  27568  lgsquadlem1  27573  lgsquadlem2  27574  lgsquadlem3  27575  chebbnd1lem1  27662  chebbnd1lem2  27663  chebbnd1lem3  27664  mulog2sumlem2  27728  pntpbnd1a  27778  pntibndlem1  27782  pntibndlem3  27785  pntlemc  27788  ostth2  27830  ostth3  27831  absmuls  28466  pthdlem1  30144  numclwlk1lem2  30750  smcnlem  31078  minvecolem2  31256  minvecolem4  31261  strlem5  32636  hstrlem5  32644  abrexdomjm  32882  prct  33087  cyc3conja  33500  elrgspnlem2  33586  mplvrpmga  33958  psrmonprod  33965  fldextrspunlsplem  34086  constrext2chnlem  34163  dya2icoseg  34691  omssubadd  34714  omsmeas  34737  oddpwdc  34768  logdivsqrle  35061  faclim  36251  faclim2  36253  taupilem1  37998  mblfinlem3  38343  mblfinlem4  38344  ibladdnclem  38360  iblmulc2nc  38369  abrexdom  38414  dalem3  40471  dalem8  40477  dalem25  40505  dalem27  40506  dalem38  40517  dalem44  40523  dalem54  40533  lhpat3  40853  4atexlemunv  40873  4atexlemtlw  40874  4atexlemc  40876  4atexlemnclw  40877  4atexlemex2  40878  4atexlemcnd  40879  cdleme0b  41019  cdleme0c  41020  cdleme0fN  41025  cdlemeulpq  41027  cdleme01N  41028  cdleme0ex1N  41030  cdleme2  41035  cdleme3b  41036  cdleme3c  41037  cdleme3g  41041  cdleme3h  41042  cdleme4a  41046  cdleme7aa  41049  cdleme7c  41052  cdleme7d  41053  cdleme7e  41054  cdleme9  41060  cdleme11fN  41071  cdleme11k  41075  cdleme15d  41084  cdlemednpq  41106  cdleme19c  41112  cdleme20aN  41116  cdleme20e  41120  cdleme21c  41134  cdleme21ct  41136  cdleme22e  41151  cdleme22eALTN  41152  cdleme22f  41153  cdleme23a  41156  cdleme28a  41177  cdleme35f  41261  cdlemeg46frv  41332  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemg2fv2  41407  cdlemg2m  41411  cdlemg6c  41427  cdlemg31a  41504  cdlemg31b  41505  cdlemk10  41650  cdlemk37  41721  dia2dimlem1  41871  dihjatcclem4  42228  imadomfi  42802  aks5lem1  42986  3cubeslem1  43448  irrapxlem3  43584  pell14qrgapw  43636  dgrsub2  43895  radcnvrat  45057  ressiooinf  46306  fmul01  46329  fmul01lt1lem1  46333  fmul01lt1lem2  46334  sumnnodd  46379  climlimsupcex  46516  cnrefiisplem  46576  stoweidlem1  46748  stoweidlem5  46752  stoweidlem7  46754  dirkercncflem1  46850  dirkercncflem4  46853  fourierdlem30  46884  fourierdlem42  46896  fourierdlem48  46901  fourierdlem49  46902  fourierdlem62  46915  fourierdlem63  46916  fourierdlem68  46921  fourierdlem79  46932  sqwvfoura  46975  etransclem32  47013  hoidmvlelem2  47343  iunhoiioolem  47422  vonioolem1  47427  pimdecfgtioo  47464  pimincfltioo  47465  smfmullem1  47538  2ltceilhalf  48102  rehalfge1  48109  m1modnep2mod  48128  difmodm1lt  48135  2timesltsqm1  48149  fmtnoge3  48315  fmtnoprmfac2lem1  48351  sfprmdvdsmersenne  48388  lighneallem2  48391  lighneallem4a  48393  proththdlem  48398  nprmdvdsfacm1lem2  48406  stgoldbwt  48574  sgoldbeven3prm  48581  mogoldbb  48583  evengpop3  48596  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  lindslinindimp2lem3  49273  fllogbd  49373  nnolog2flm1  49403