Theorem eqbrtrid 5135

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  map1  8989  xp1en  9003  map2xp  9087  rex2dom  9165  sucxpdom  9173  sniffsupp  9315  wdomima2g  9503  endjudisj  10091  dju1dif  10095  mapdjuen  10103  djuxpdom  10108  djufi  10109  pwsdompw  10125  infunsdom1  10134  infunsdom  10135  infxp  10136  ackbij1lem5  10145  hsmexlem4  10351  imadomg  10456  unidom  10465  unictb  10498  pwxpndom2  10588  pwdjundom  10590  distrnq  10884  nnne0  12191  supxrmnf  13244  xov1plusxeqvd  13426  quoremz  13787  quoremnn0ALT  13789  intfrac2  13790  m1modge3gt1  13853  bernneq2  14165  faclbnd4lem1  14228  01sqrexlem4  15180  reccn2  15532  caucvg  15614  o1fsum  15748  infcvgaux2i  15793  eirrlem  16141  rpnnen2lem12  16162  ruclem12  16178  nno  16321  divalglem5  16336  bitsfzolem  16373  bitsinv1lem  16380  bezoutlem3  16480  lcmfunsnlem  16580  coprmproddvds  16602  oddprmge3  16639  ge2nprmge4  16640  sqnprm  16641  prmreclem6  16861  4sqlem6  16883  4sqlem13  16897  4sqlem16  16900  4sqlem17  16901  2expltfac  17032  odcau  19545  sylow3  19574  efginvrel2  19668  lt6abl  19836  ablfac1lem  20011  gzrngunitlem  21399  zringlpirlem3  21431  dvdschrmulg  21495  znfld  21527  evlslem2  22046  chfacffsupp  22812  cpmidpmatlem3  22828  cctop  22962  csdfil  23850  xpsdsval  24337  nrginvrcnlem  24647  icccmplem2  24780  reconnlem2  24784  iscmet3lem3  25258  minveclem2  25394  minveclem4  25400  ivthlem2  25421  ivthlem3  25422  ovolunlem1a  25465  ovolfiniun  25470  ovoliunlem3  25473  ovoliun  25474  ovolicc2lem4  25489  unmbl  25506  ioombl1lem4  25530  itg2mono  25722  ibladdlem  25789  iblabsr  25799  iblmulc2  25800  bddiblnc  25811  dvferm1lem  25956  dvferm2lem  25958  lhop1lem  25986  dvcvx  25993  ftc1a  26012  plyeq0lem  26183  aannenlem3  26306  geolim3  26315  psercnlem1  26403  pserdvlem2  26406  reeff1olem  26424  pilem2  26430  pilem3  26431  cosq14gt0  26487  cosq14ge0  26488  cosne0  26506  recosf1o  26512  resinf1o  26513  argregt0  26587  logcnlem3  26621  logcnlem4  26622  logf1o2  26627  cxpcn3lem  26725  ang180lem2  26788  acosbnd  26878  atanbndlem  26903  leibpi  26920  cxp2lim  26955  emcllem2  26975  ftalem5  27055  basellem9  27067  vmage0  27099  chpge0  27104  chtub  27191  mersenne  27206  bposlem2  27264  bposlem5  27267  bposlem6  27268  bposlem9  27271  gausslemma2dlem0c  27337  gausslemma2dlem0e  27339  lgseisenlem1  27354  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  mulog2sumlem2  27514  pntpbnd1a  27564  pntibndlem1  27568  pntibndlem3  27571  pntlemc  27574  ostth2  27616  ostth3  27617  absmuls  28252  pthdlem1  29851  numclwlk1lem2  30457  smcnlem  30784  minvecolem2  30962  minvecolem4  30967  strlem5  32342  hstrlem5  32350  abrexdomjm  32593  prct  32802  cyc3conja  33250  elrgspnlem2  33336  prmidl0  33542  mplvrpmga  33721  psrmonprod  33728  fldextrspunlsplem  33850  constrext2chnlem  33927  dya2icoseg  34454  omssubadd  34477  omsmeas  34500  oddpwdc  34531  logdivsqrle  34827  faclim  35959  faclim2  35961  taupilem1  37573  mblfinlem3  37907  mblfinlem4  37908  ibladdnclem  37924  iblmulc2nc  37933  abrexdom  37978  dalem3  40037  dalem8  40043  dalem25  40071  dalem27  40072  dalem38  40083  dalem44  40089  dalem54  40099  lhpat3  40419  4atexlemunv  40439  4atexlemtlw  40440  4atexlemc  40442  4atexlemnclw  40443  4atexlemex2  40444  4atexlemcnd  40445  cdleme0b  40585  cdleme0c  40586  cdleme0fN  40591  cdlemeulpq  40593  cdleme01N  40594  cdleme0ex1N  40596  cdleme2  40601  cdleme3b  40602  cdleme3c  40603  cdleme3g  40607  cdleme3h  40608  cdleme4a  40612  cdleme7aa  40615  cdleme7c  40618  cdleme7d  40619  cdleme7e  40620  cdleme9  40626  cdleme11fN  40637  cdleme11k  40641  cdleme15d  40650  cdlemednpq  40672  cdleme19c  40678  cdleme20aN  40682  cdleme20e  40686  cdleme21c  40700  cdleme21ct  40702  cdleme22e  40717  cdleme22eALTN  40718  cdleme22f  40719  cdleme23a  40722  cdleme28a  40743  cdleme35f  40827  cdlemeg46frv  40898  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemg2fv2  40973  cdlemg2m  40977  cdlemg6c  40993  cdlemg31a  41070  cdlemg31b  41071  cdlemk10  41216  cdlemk37  41287  dia2dimlem1  41437  dihjatcclem4  41794  imadomfi  42369  aks5lem1  42553  3cubeslem1  43038  irrapxlem3  43178  pell14qrgapw  43230  dgrsub2  43489  radcnvrat  44667  ressiooinf  45914  fmul01  45937  fmul01lt1lem1  45941  fmul01lt1lem2  45942  sumnnodd  45987  climlimsupcex  46124  cnrefiisplem  46184  stoweidlem1  46356  stoweidlem5  46360  stoweidlem7  46362  dirkercncflem1  46458  dirkercncflem4  46461  fourierdlem30  46492  fourierdlem42  46504  fourierdlem48  46509  fourierdlem62  46523  fourierdlem63  46524  fourierdlem68  46529  fourierdlem79  46540  sqwvfoura  46583  etransclem32  46621  hoidmvlelem2  46951  iunhoiioolem  47030  vonioolem1  47035  pimdecfgtioo  47072  pimincfltioo  47073  smfmullem1  47146  2ltceilhalf  47685  rehalfge1  47692  m1modnep2mod  47709  difmodm1lt  47716  fmtnoge3  47887  fmtnoprmfac2lem1  47923  sfprmdvdsmersenne  47960  lighneallem2  47963  lighneallem4a  47965  proththdlem  47970  stgoldbwt  48133  sgoldbeven3prm  48140  mogoldbb  48142  evengpop3  48155  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  lindslinindimp2lem3  48817  fllogbd  48917  nnolog2flm1  48947