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  39330  irrapxlem3  39470  pell14qrgapw  39522  dgrsub2  39784  radcnvrat  40695  ressiooinf  41882  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1lem2  41915  sumnnodd  41960  climlimsupcex  42099  cnrefiisplem  42159  stoweidlem1  42335  stoweidlem5  42339  stoweidlem7  42341  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem30  42471  fourierdlem42  42483  fourierdlem48  42488  fourierdlem62  42502  fourierdlem63  42503  fourierdlem68  42508  fourierdlem79  42519  sqwvfoura  42562  etransclem32  42600  hoidmvlelem2  42927  iunhoiioolem  43006  vonioolem1  43011  pimdecfgtioo  43044  pimincfltioo  43045  smfmullem1  43115  fmtnoge3  43741  fmtnoprmfac2lem1  43777  sfprmdvdsmersenne  43817  lighneallem2  43820  lighneallem4a  43822  proththdlem  43827  stgoldbwt  43990  sgoldbeven3prm  43997  mogoldbb  43999  evengpop3  44012  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  lindslinindimp2lem3  44564  fllogbd  44669  nnolog2flm1  44699