Theorem eqbrtrid 5139

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  map1  9072  xp1en  9086  map2xp  9170  rex2dom  9248  sucxpdom  9256  sniffsupp  9396  wdomima2g  9584  endjudisj  10251  dju1dif  10255  mapdjuen  10263  djuxpdom  10268  djufi  10269  pwsdompw  10285  infunsdom1  10294  infunsdom  10295  infxp  10296  ackbij1lem5  10305  hsmexlem4  10511  imadomg  10617  imadomnum  10618  unidom  10631  unictb  10664  pwxpndom2  10754  pwdjundom  10756  distrnq  11050  nnne0  12376  supxrmnf  13451  xov1plusxeqvd  13633  quoremz  13999  quoremnn0ALT  14001  intfrac2  14002  m1modge3gt1  14065  bernneq2  14378  faclbnd4lem1  14441  01sqrexlem4  15418  reccn2  15770  caucvg  15852  o1fsum  15986  infcvgaux2i  16033  eirrlem  16378  rpnnen2lem12  16399  ruclem12  16415  nno  16558  divalglem5  16573  bitsfzolem  16610  bitsinv1lem  16617  bezoutlem3  16720  lcmfunsnlem  16822  coprmproddvds  16844  oddprmge3  16882  ge2nprmge4  16883  sqnprm  16884  prmreclem6  17105  4sqlem6  17127  4sqlem13  17141  4sqlem16  17144  4sqlem17  17145  2expltfac  17276  odcau  19824  sylow3  19853  efginvrel2  19947  lt6abl  20115  ablfac1lem  20290  prmidl0  21640  gzrngunitlem  21744  zringlpirlem3  21776  dvdschrmulg  21840  znfld  21872  evlslem2  22394  chfacffsupp  23180  cpmidpmatlem3  23196  cctop  23330  csdfil  24219  xpsdsval  24706  nrginvrcnlem  25016  icccmplem2  25149  reconnlem2  25153  iscmet3lem3  25617  minveclem2  25753  minveclem4  25759  ivthlem2  25779  ivthlem3  25780  ovolunlem1a  25823  ovolfiniun  25828  ovoliunlem3  25831  ovoliun  25832  ovolicc2lem4  25847  unmbl  25864  ioombl1lem4  25888  itg2mono  26080  ibladdlem  26146  iblabsr  26156  iblmulc2  26157  bddiblnc  26168  dvferm1lem  26310  dvferm2lem  26312  lhop1lem  26339  dvcvx  26346  ftc1a  26363  plyeq0lem  26535  aannenlem3  26663  geolim3  26672  psercnlem1  26758  pserdvlem2  26761  reeff1olem  26779  pilem2  26785  pilem3  26786  cosq14gt0  26845  cosq14ge0  26846  cosne0  26863  recosf1o  26869  resinf1o  26870  argregt0  26944  logcnlem3  26978  logcnlem4  26979  logf1o2  26984  cxpcn3lem  27081  ang180lem2  27144  acosbnd  27234  atanbndlem  27259  leibpi  27276  cxp2lim  27310  emcllem2  27330  ftalem5  27410  basellem9  27422  vmage0  27454  chpge0  27459  chtub  27545  mersenne  27560  bposlem2  27618  bposlem5  27621  bposlem6  27622  bposlem9  27625  gausslemma2dlem0c  27691  gausslemma2dlem0e  27693  lgseisenlem1  27708  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  chebbnd1lem1  27802  chebbnd1lem2  27803  chebbnd1lem3  27804  mulog2sumlem2  27868  pntpbnd1a  27918  pntibndlem1  27922  pntibndlem3  27925  pntlemc  27928  ostth2  27970  ostth3  27971  fltoprmlem2  28000  absmuls  28636  pthdlem1  30358  numclwlk1lem2  30977  smcnlem  31305  minvecolem2  31483  minvecolem4  31488  strlem5  32863  hstrlem5  32871  abrexdomjm  33151  prct  33354  cyc3conja  33765  elrgspnlem2  33851  mplvrpmga  34224  psrmonprod  34231  fldextrspunlsplem  34352  constrext2chnlem  34429  dya2icoseg  34956  omssubadd  34979  omsmeas  35002  oddpwdc  35033  logdivsqrle  35326  faclim  36604  faclim2  36606  taupilem1  38336  mblfinlem3  38671  mblfinlem4  38672  ibladdnclem  38688  iblmulc2nc  38697  abrexdom  38758  dalem3  40815  dalem8  40821  dalem25  40849  dalem27  40850  dalem38  40861  dalem44  40867  dalem54  40877  lhpat3  41197  4atexlemunv  41217  4atexlemtlw  41218  4atexlemc  41220  4atexlemnclw  41221  4atexlemex2  41222  4atexlemcnd  41223  cdleme0b  41363  cdleme0c  41364  cdleme0fN  41369  cdlemeulpq  41371  cdleme01N  41372  cdleme0ex1N  41374  cdleme2  41379  cdleme3b  41380  cdleme3c  41381  cdleme3g  41385  cdleme3h  41386  cdleme4a  41390  cdleme7aa  41393  cdleme7c  41396  cdleme7d  41397  cdleme7e  41398  cdleme9  41404  cdleme11fN  41415  cdleme11k  41419  cdleme15d  41428  cdlemednpq  41450  cdleme19c  41456  cdleme20aN  41460  cdleme20e  41464  cdleme21c  41478  cdleme21ct  41480  cdleme22e  41495  cdleme22eALTN  41496  cdleme22f  41497  cdleme23a  41500  cdleme28a  41521  cdleme35f  41605  cdlemeg46frv  41676  cdlemeg46rgv  41679  cdlemeg46req  41680  cdlemg2fv2  41751  cdlemg2m  41755  cdlemg6c  41771  cdlemg31a  41848  cdlemg31b  41849  cdlemk10  41994  cdlemk37  42065  dia2dimlem1  42215  dihjatcclem4  42572  imadomfi  43146  aks5lem1  43330  3cubeslem1  43788  irrapxlem3  43925  pell14qrgapw  43977  dgrsub2  44231  radcnvrat  45392  ressiooinf  46663  fmul01  46686  fmul01lt1lem1  46690  fmul01lt1lem2  46691  sumnnodd  46736  climlimsupcex  46873  cnrefiisplem  46933  stoweidlem1  47105  stoweidlem5  47109  stoweidlem7  47111  dirkercncflem1  47207  dirkercncflem4  47210  fourierdlem30  47241  fourierdlem42  47253  fourierdlem48  47258  fourierdlem49  47259  fourierdlem62  47272  fourierdlem63  47273  fourierdlem68  47278  fourierdlem79  47289  sqwvfoura  47332  etransclem32  47370  hoidmvlelem2  47700  iunhoiioolem  47779  vonioolem1  47784  pimdecfgtioo  47821  pimincfltioo  47822  smfmullem1  47895  2ltceilhalf  48496  rehalfge1  48503  m1modnep2mod  48522  difmodm1lt  48529  2timesltsqm1  48543  fmtnoge3  48709  fmtnoprmfac2lem1  48745  sfprmdvdsmersenne  48782  lighneallem2  48785  lighneallem4a  48787  proththdlem  48792  nprmdvdsfacm1lem2  48800  stgoldbwt  48968  sgoldbeven3prm  48975  mogoldbb  48977  evengpop3  48990  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  lindslinindimp2lem3  49666  fllogbd  49766  nnolog2flm1  49796