Theorem eqbrtrid 5101

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5066

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067

This theorem is referenced by:  map1  8592  xp1en  8603  map2xp  8687  1sdom  8721  sucxpdom  8727  sniffsupp  8873  wdomima2g  9050  endjudisj  9594  dju1dif  9598  mapdjuen  9606  djuxpdom  9611  djufi  9612  pwsdompw  9626  infunsdom1  9635  infunsdom  9636  infxp  9637  ackbij1lem5  9646  hsmexlem4  9851  imadomg  9956  unidom  9965  unictb  9997  pwxpndom2  10087  pwdjundom  10089  distrnq  10383  nnne0  11672  supxrmnf  12711  xov1plusxeqvd  12885  quoremz  13224  quoremnn0ALT  13226  intfrac2  13227  m1modge3gt1  13287  bernneq2  13592  faclbnd4lem1  13654  sqrlem4  14605  reccn2  14953  caucvg  15035  o1fsum  15168  infcvgaux2i  15213  eirrlem  15557  rpnnen2lem12  15578  ruclem12  15594  nno  15733  divalglem5  15748  bitsfzolem  15783  bitsinv1lem  15790  bezoutlem3  15889  lcmfunsnlem  15985  coprmproddvds  16007  oddprmge3  16044  ge2nprmge4  16045  sqnprm  16046  prmreclem6  16257  4sqlem6  16279  4sqlem13  16293  4sqlem16  16296  4sqlem17  16297  2expltfac  16426  odcau  18729  sylow3  18758  efginvrel2  18853  lt6abl  19015  ablfac1lem  19190  evlslem2  20292  gzrngunitlem  20610  zringlpirlem3  20633  znfld  20707  chfacffsupp  21464  cpmidpmatlem3  21480  cctop  21614  csdfil  22502  xpsdsval  22991  nrginvrcnlem  23300  icccmplem2  23431  reconnlem2  23435  iscmet3lem3  23893  minveclem2  24029  minveclem4  24035  ivthlem2  24053  ivthlem3  24054  ovolunlem1a  24097  ovolfiniun  24102  ovoliunlem3  24105  ovoliun  24106  ovolicc2lem4  24121  unmbl  24138  ioombl1lem4  24162  itg2mono  24354  ibladdlem  24420  iblabsr  24430  iblmulc2  24431  dvferm1lem  24581  dvferm2lem  24583  lhop1lem  24610  dvcvx  24617  ftc1a  24634  plyeq0lem  24800  aannenlem3  24919  geolim3  24928  psercnlem1  25013  pserdvlem2  25016  reeff1olem  25034  pilem2  25040  pilem3  25041  cosq14gt0  25096  cosq14ge0  25097  cosne0  25114  recosf1o  25119  resinf1o  25120  argregt0  25193  logcnlem3  25227  logcnlem4  25228  logf1o2  25233  cxpcn3lem  25328  ang180lem2  25388  acosbnd  25478  atanbndlem  25503  leibpi  25520  cxp2lim  25554  emcllem2  25574  ftalem5  25654  basellem9  25666  vmage0  25698  chpge0  25703  chtub  25788  mersenne  25803  bposlem2  25861  bposlem5  25864  bposlem6  25865  bposlem9  25868  gausslemma2dlem0c  25934  gausslemma2dlem0e  25936  lgseisenlem1  25951  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  mulog2sumlem2  26111  pntpbnd1a  26161  pntibndlem1  26165  pntibndlem3  26168  pntlemc  26171  ostth2  26213  ostth3  26214  pthdlem1  27547  numclwlk1lem2  28149  smcnlem  28474  minvecolem2  28652  minvecolem4  28657  strlem5  30032  hstrlem5  30040  abrexdomjm  30267  prct  30450  cyc3conja  30799  dvdschrmulg  30858  dya2icoseg  31535  omssubadd  31558  omsmeas  31581  oddpwdc  31612  logdivsqrle  31921  faclim  32978  faclim2  32980  taupilem1  34605  mblfinlem3  34946  mblfinlem4  34947  ibladdnclem  34963  iblmulc2nc  34972  bddiblnc  34977  abrexdom  35020  dalem3  36815  dalem8  36821  dalem25  36849  dalem27  36850  dalem38  36861  dalem44  36867  dalem54  36877  lhpat3  37197  4atexlemunv  37217  4atexlemtlw  37218  4atexlemc  37220  4atexlemnclw  37221  4atexlemex2  37222  4atexlemcnd  37223  cdleme0b  37363  cdleme0c  37364  cdleme0fN  37369  cdlemeulpq  37371  cdleme01N  37372  cdleme0ex1N  37374  cdleme2  37379  cdleme3b  37380  cdleme3c  37381  cdleme3g  37385  cdleme3h  37386  cdleme4a  37390  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme9  37404  cdleme11fN  37415  cdleme11k  37419  cdleme15d  37428  cdlemednpq  37450  cdleme19c  37456  cdleme20aN  37460  cdleme20e  37464  cdleme21c  37478  cdleme21ct  37480  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme23a  37500  cdleme28a  37521  cdleme35f  37605  cdlemeg46frv  37676  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg6c  37771  cdlemg31a  37848  cdlemg31b  37849  cdlemk10  37994  cdlemk37  38065  dia2dimlem1  38215  dihjatcclem4  38572  3cubeslem1  39301  irrapxlem3  39441  pell14qrgapw  39493  dgrsub2  39755  radcnvrat  40666  ressiooinf  41853  fmul01  41881  fmul01lt1lem1  41885  fmul01lt1lem2  41886  sumnnodd  41931  climlimsupcex  42070  cnrefiisplem  42130  stoweidlem1  42306  stoweidlem5  42310  stoweidlem7  42312  dirkercncflem1  42408  dirkercncflem4  42411  fourierdlem30  42442  fourierdlem42  42454  fourierdlem48  42459  fourierdlem62  42473  fourierdlem63  42474  fourierdlem68  42479  fourierdlem79  42490  sqwvfoura  42533  etransclem32  42571  hoidmvlelem2  42898  iunhoiioolem  42977  vonioolem1  42982  pimdecfgtioo  43015  pimincfltioo  43016  smfmullem1  43086  fmtnoge3  43712  fmtnoprmfac2lem1  43748  sfprmdvdsmersenne  43788  lighneallem2  43791  lighneallem4a  43793  proththdlem  43798  stgoldbwt  43961  sgoldbeven3prm  43968  mogoldbb  43970  evengpop3  43983  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  lindslinindimp2lem3  44535  fllogbd  44640  nnolog2flm1  44670