Theorem eqbrtrid 5133

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  map1  8977  xp1en  8991  map2xp  9075  rex2dom  9153  sucxpdom  9161  sniffsupp  9303  wdomima2g  9491  endjudisj  10079  dju1dif  10083  mapdjuen  10091  djuxpdom  10096  djufi  10097  pwsdompw  10113  infunsdom1  10122  infunsdom  10123  infxp  10124  ackbij1lem5  10133  hsmexlem4  10339  imadomg  10444  unidom  10453  unictb  10486  pwxpndom2  10576  pwdjundom  10578  distrnq  10872  nnne0  12179  supxrmnf  13232  xov1plusxeqvd  13414  quoremz  13775  quoremnn0ALT  13777  intfrac2  13778  m1modge3gt1  13841  bernneq2  14153  faclbnd4lem1  14216  01sqrexlem4  15168  reccn2  15520  caucvg  15602  o1fsum  15736  infcvgaux2i  15781  eirrlem  16129  rpnnen2lem12  16150  ruclem12  16166  nno  16309  divalglem5  16324  bitsfzolem  16361  bitsinv1lem  16368  bezoutlem3  16468  lcmfunsnlem  16568  coprmproddvds  16590  oddprmge3  16627  ge2nprmge4  16628  sqnprm  16629  prmreclem6  16849  4sqlem6  16871  4sqlem13  16885  4sqlem16  16888  4sqlem17  16889  2expltfac  17020  odcau  19533  sylow3  19562  efginvrel2  19656  lt6abl  19824  ablfac1lem  19999  gzrngunitlem  21387  zringlpirlem3  21419  dvdschrmulg  21483  znfld  21515  evlslem2  22034  chfacffsupp  22800  cpmidpmatlem3  22816  cctop  22950  csdfil  23838  xpsdsval  24325  nrginvrcnlem  24635  icccmplem2  24768  reconnlem2  24772  iscmet3lem3  25246  minveclem2  25382  minveclem4  25388  ivthlem2  25409  ivthlem3  25410  ovolunlem1a  25453  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovolicc2lem4  25477  unmbl  25494  ioombl1lem4  25518  itg2mono  25710  ibladdlem  25777  iblabsr  25787  iblmulc2  25788  bddiblnc  25799  dvferm1lem  25944  dvferm2lem  25946  lhop1lem  25974  dvcvx  25981  ftc1a  26000  plyeq0lem  26171  aannenlem3  26294  geolim3  26303  psercnlem1  26391  pserdvlem2  26394  reeff1olem  26412  pilem2  26418  pilem3  26419  cosq14gt0  26475  cosq14ge0  26476  cosne0  26494  recosf1o  26500  resinf1o  26501  argregt0  26575  logcnlem3  26609  logcnlem4  26610  logf1o2  26615  cxpcn3lem  26713  ang180lem2  26776  acosbnd  26866  atanbndlem  26891  leibpi  26908  cxp2lim  26943  emcllem2  26963  ftalem5  27043  basellem9  27055  vmage0  27087  chpge0  27092  chtub  27179  mersenne  27194  bposlem2  27252  bposlem5  27255  bposlem6  27256  bposlem9  27259  gausslemma2dlem0c  27325  gausslemma2dlem0e  27327  lgseisenlem1  27342  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  mulog2sumlem2  27502  pntpbnd1a  27552  pntibndlem1  27556  pntibndlem3  27559  pntlemc  27562  ostth2  27604  ostth3  27605  absmuls  28240  pthdlem1  29839  numclwlk1lem2  30445  smcnlem  30772  minvecolem2  30950  minvecolem4  30955  strlem5  32330  hstrlem5  32338  abrexdomjm  32582  prct  32792  cyc3conja  33239  elrgspnlem2  33325  prmidl0  33531  mplvrpmga  33710  fldextrspunlsplem  33830  constrext2chnlem  33907  dya2icoseg  34434  omssubadd  34457  omsmeas  34480  oddpwdc  34511  logdivsqrle  34807  faclim  35940  faclim2  35942  taupilem1  37526  mblfinlem3  37860  mblfinlem4  37861  ibladdnclem  37877  iblmulc2nc  37886  abrexdom  37931  dalem3  39924  dalem8  39930  dalem25  39958  dalem27  39959  dalem38  39970  dalem44  39976  dalem54  39986  lhpat3  40306  4atexlemunv  40326  4atexlemtlw  40327  4atexlemc  40329  4atexlemnclw  40330  4atexlemex2  40331  4atexlemcnd  40332  cdleme0b  40472  cdleme0c  40473  cdleme0fN  40478  cdlemeulpq  40480  cdleme01N  40481  cdleme0ex1N  40483  cdleme2  40488  cdleme3b  40489  cdleme3c  40490  cdleme3g  40494  cdleme3h  40495  cdleme4a  40499  cdleme7aa  40502  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme9  40513  cdleme11fN  40524  cdleme11k  40528  cdleme15d  40537  cdlemednpq  40559  cdleme19c  40565  cdleme20aN  40569  cdleme20e  40573  cdleme21c  40587  cdleme21ct  40589  cdleme22e  40604  cdleme22eALTN  40605  cdleme22f  40606  cdleme23a  40609  cdleme28a  40630  cdleme35f  40714  cdlemeg46frv  40785  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemg2fv2  40860  cdlemg2m  40864  cdlemg6c  40880  cdlemg31a  40957  cdlemg31b  40958  cdlemk10  41103  cdlemk37  41174  dia2dimlem1  41324  dihjatcclem4  41681  imadomfi  42256  aks5lem1  42440  3cubeslem1  42926  irrapxlem3  43066  pell14qrgapw  43118  dgrsub2  43377  radcnvrat  44555  ressiooinf  45803  fmul01  45826  fmul01lt1lem1  45830  fmul01lt1lem2  45831  sumnnodd  45876  climlimsupcex  46013  cnrefiisplem  46073  stoweidlem1  46245  stoweidlem5  46249  stoweidlem7  46251  dirkercncflem1  46347  dirkercncflem4  46350  fourierdlem30  46381  fourierdlem42  46393  fourierdlem48  46398  fourierdlem62  46412  fourierdlem63  46413  fourierdlem68  46418  fourierdlem79  46429  sqwvfoura  46472  etransclem32  46510  hoidmvlelem2  46840  iunhoiioolem  46919  vonioolem1  46924  pimdecfgtioo  46961  pimincfltioo  46962  smfmullem1  47035  2ltceilhalf  47574  rehalfge1  47581  m1modnep2mod  47598  difmodm1lt  47605  fmtnoge3  47776  fmtnoprmfac2lem1  47812  sfprmdvdsmersenne  47849  lighneallem2  47852  lighneallem4a  47854  proththdlem  47859  stgoldbwt  48022  sgoldbeven3prm  48029  mogoldbb  48031  evengpop3  48044  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  lindslinindimp2lem3  48706  fllogbd  48806  nnolog2flm1  48836