Theorem eqbrtrid 5177

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 5176	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  map1  9081  xp1en  9098  map2xp  9188  rex2dom  9283  1sdomOLD  9286  sucxpdom  9292  sniffsupp  9441  wdomima2g  9627  endjudisj  10210  dju1dif  10214  mapdjuen  10222  djuxpdom  10227  djufi  10228  pwsdompw  10244  infunsdom1  10253  infunsdom  10254  infxp  10255  ackbij1lem5  10264  hsmexlem4  10470  imadomg  10575  unidom  10584  unictb  10616  pwxpndom2  10706  pwdjundom  10708  distrnq  11002  nnne0  12301  supxrmnf  13360  xov1plusxeqvd  13539  quoremz  13896  quoremnn0ALT  13898  intfrac2  13899  m1modge3gt1  13960  bernneq2  14270  faclbnd4lem1  14333  01sqrexlem4  15285  reccn2  15634  caucvg  15716  o1fsum  15850  infcvgaux2i  15895  eirrlem  16241  rpnnen2lem12  16262  ruclem12  16278  nno  16420  divalglem5  16435  bitsfzolem  16472  bitsinv1lem  16479  bezoutlem3  16579  lcmfunsnlem  16679  coprmproddvds  16701  oddprmge3  16738  ge2nprmge4  16739  sqnprm  16740  prmreclem6  16960  4sqlem6  16982  4sqlem13  16996  4sqlem16  16999  4sqlem17  17000  2expltfac  17131  odcau  19623  sylow3  19652  efginvrel2  19746  lt6abl  19914  ablfac1lem  20089  gzrngunitlem  21451  zringlpirlem3  21476  dvdschrmulg  21544  znfld  21580  evlslem2  22104  chfacffsupp  22863  cpmidpmatlem3  22879  cctop  23014  csdfil  23903  xpsdsval  24392  nrginvrcnlem  24713  icccmplem2  24846  reconnlem2  24850  iscmet3lem3  25325  minveclem2  25461  minveclem4  25467  ivthlem2  25488  ivthlem3  25489  ovolunlem1a  25532  ovolfiniun  25537  ovoliunlem3  25540  ovoliun  25541  ovolicc2lem4  25556  unmbl  25573  ioombl1lem4  25597  itg2mono  25789  ibladdlem  25856  iblabsr  25866  iblmulc2  25867  bddiblnc  25878  dvferm1lem  26023  dvferm2lem  26025  lhop1lem  26053  dvcvx  26060  ftc1a  26079  plyeq0lem  26250  aannenlem3  26373  geolim3  26382  psercnlem1  26470  pserdvlem2  26473  reeff1olem  26491  pilem2  26497  pilem3  26498  cosq14gt0  26553  cosq14ge0  26554  cosne0  26572  recosf1o  26578  resinf1o  26579  argregt0  26653  logcnlem3  26687  logcnlem4  26688  logf1o2  26693  cxpcn3lem  26791  ang180lem2  26854  acosbnd  26944  atanbndlem  26969  leibpi  26986  cxp2lim  27021  emcllem2  27041  ftalem5  27121  basellem9  27133  vmage0  27165  chpge0  27170  chtub  27257  mersenne  27272  bposlem2  27330  bposlem5  27333  bposlem6  27334  bposlem9  27337  gausslemma2dlem0c  27403  gausslemma2dlem0e  27405  lgseisenlem1  27420  lgsquadlem1  27425  lgsquadlem2  27426  lgsquadlem3  27427  chebbnd1lem1  27514  chebbnd1lem2  27515  chebbnd1lem3  27516  mulog2sumlem2  27580  pntpbnd1a  27630  pntibndlem1  27634  pntibndlem3  27637  pntlemc  27640  ostth2  27682  ostth3  27683  absmuls  28269  pthdlem1  29787  numclwlk1lem2  30390  smcnlem  30717  minvecolem2  30895  minvecolem4  30900  strlem5  32275  hstrlem5  32283  abrexdomjm  32527  prct  32727  cyc3conja  33178  elrgspnlem2  33248  prmidl0  33479  fldextrspunlsplem  33724  dya2icoseg  34280  omssubadd  34303  omsmeas  34326  oddpwdc  34357  logdivsqrle  34666  faclim  35747  faclim2  35749  taupilem1  37323  mblfinlem3  37667  mblfinlem4  37668  ibladdnclem  37684  iblmulc2nc  37693  abrexdom  37738  dalem3  39667  dalem8  39673  dalem25  39701  dalem27  39702  dalem38  39713  dalem44  39719  dalem54  39729  lhpat3  40049  4atexlemunv  40069  4atexlemtlw  40070  4atexlemc  40072  4atexlemnclw  40073  4atexlemex2  40074  4atexlemcnd  40075  cdleme0b  40215  cdleme0c  40216  cdleme0fN  40221  cdlemeulpq  40223  cdleme01N  40224  cdleme0ex1N  40226  cdleme2  40231  cdleme3b  40232  cdleme3c  40233  cdleme3g  40237  cdleme3h  40238  cdleme4a  40242  cdleme7aa  40245  cdleme7c  40248  cdleme7d  40249  cdleme7e  40250  cdleme9  40256  cdleme11fN  40267  cdleme11k  40271  cdleme15d  40280  cdlemednpq  40302  cdleme19c  40308  cdleme20aN  40312  cdleme20e  40316  cdleme21c  40330  cdleme21ct  40332  cdleme22e  40347  cdleme22eALTN  40348  cdleme22f  40349  cdleme23a  40352  cdleme28a  40373  cdleme35f  40457  cdlemeg46frv  40528  cdlemeg46rgv  40531  cdlemeg46req  40532  cdlemg2fv2  40603  cdlemg2m  40607  cdlemg6c  40623  cdlemg31a  40700  cdlemg31b  40701  cdlemk10  40846  cdlemk37  40917  dia2dimlem1  41067  dihjatcclem4  41424  imadomfi  42004  aks5lem1  42188  metakunt30  42236  3cubeslem1  42700  irrapxlem3  42840  pell14qrgapw  42892  dgrsub2  43152  radcnvrat  44338  ressiooinf  45575  fmul01  45600  fmul01lt1lem1  45604  fmul01lt1lem2  45605  sumnnodd  45650  climlimsupcex  45789  cnrefiisplem  45849  stoweidlem1  46021  stoweidlem5  46025  stoweidlem7  46027  dirkercncflem1  46123  dirkercncflem4  46126  fourierdlem30  46157  fourierdlem42  46169  fourierdlem48  46174  fourierdlem62  46188  fourierdlem63  46189  fourierdlem68  46194  fourierdlem79  46205  sqwvfoura  46248  etransclem32  46286  hoidmvlelem2  46616  iunhoiioolem  46695  vonioolem1  46700  pimdecfgtioo  46737  pimincfltioo  46738  smfmullem1  46811  m1modnep2mod  47359  fmtnoge3  47522  fmtnoprmfac2lem1  47558  sfprmdvdsmersenne  47595  lighneallem2  47598  lighneallem4a  47600  proththdlem  47605  stgoldbwt  47768  sgoldbeven3prm  47775  mogoldbb  47777  evengpop3  47790  bgoldbtbndlem2  47798  bgoldbtbndlem3  47799  2ltceilhalf  48020  lindslinindimp2lem3  48382  fllogbd  48486  nnolog2flm1  48516