Theorem eqbrtrid 5142

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  map1  9011  xp1en  9027  map2xp  9111  rex2dom  9193  1sdomOLD  9196  sucxpdom  9202  sniffsupp  9351  wdomima2g  9539  endjudisj  10122  dju1dif  10126  mapdjuen  10134  djuxpdom  10139  djufi  10140  pwsdompw  10156  infunsdom1  10165  infunsdom  10166  infxp  10167  ackbij1lem5  10176  hsmexlem4  10382  imadomg  10487  unidom  10496  unictb  10528  pwxpndom2  10618  pwdjundom  10620  distrnq  10914  nnne0  12220  supxrmnf  13277  xov1plusxeqvd  13459  quoremz  13817  quoremnn0ALT  13819  intfrac2  13820  m1modge3gt1  13883  bernneq2  14195  faclbnd4lem1  14258  01sqrexlem4  15211  reccn2  15563  caucvg  15645  o1fsum  15779  infcvgaux2i  15824  eirrlem  16172  rpnnen2lem12  16193  ruclem12  16209  nno  16352  divalglem5  16367  bitsfzolem  16404  bitsinv1lem  16411  bezoutlem3  16511  lcmfunsnlem  16611  coprmproddvds  16633  oddprmge3  16670  ge2nprmge4  16671  sqnprm  16672  prmreclem6  16892  4sqlem6  16914  4sqlem13  16928  4sqlem16  16931  4sqlem17  16932  2expltfac  17063  odcau  19534  sylow3  19563  efginvrel2  19657  lt6abl  19825  ablfac1lem  20000  gzrngunitlem  21349  zringlpirlem3  21374  dvdschrmulg  21438  znfld  21470  evlslem2  21986  chfacffsupp  22743  cpmidpmatlem3  22759  cctop  22893  csdfil  23781  xpsdsval  24269  nrginvrcnlem  24579  icccmplem2  24712  reconnlem2  24716  iscmet3lem3  25190  minveclem2  25326  minveclem4  25332  ivthlem2  25353  ivthlem3  25354  ovolunlem1a  25397  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovolicc2lem4  25421  unmbl  25438  ioombl1lem4  25462  itg2mono  25654  ibladdlem  25721  iblabsr  25731  iblmulc2  25732  bddiblnc  25743  dvferm1lem  25888  dvferm2lem  25890  lhop1lem  25918  dvcvx  25925  ftc1a  25944  plyeq0lem  26115  aannenlem3  26238  geolim3  26247  psercnlem1  26335  pserdvlem2  26338  reeff1olem  26356  pilem2  26362  pilem3  26363  cosq14gt0  26419  cosq14ge0  26420  cosne0  26438  recosf1o  26444  resinf1o  26445  argregt0  26519  logcnlem3  26553  logcnlem4  26554  logf1o2  26559  cxpcn3lem  26657  ang180lem2  26720  acosbnd  26810  atanbndlem  26835  leibpi  26852  cxp2lim  26887  emcllem2  26907  ftalem5  26987  basellem9  26999  vmage0  27031  chpge0  27036  chtub  27123  mersenne  27138  bposlem2  27196  bposlem5  27199  bposlem6  27200  bposlem9  27203  gausslemma2dlem0c  27269  gausslemma2dlem0e  27271  lgseisenlem1  27286  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  mulog2sumlem2  27446  pntpbnd1a  27496  pntibndlem1  27500  pntibndlem3  27503  pntlemc  27506  ostth2  27548  ostth3  27549  absmuls  28146  pthdlem1  29696  numclwlk1lem2  30299  smcnlem  30626  minvecolem2  30804  minvecolem4  30809  strlem5  32184  hstrlem5  32192  abrexdomjm  32436  prct  32638  cyc3conja  33114  elrgspnlem2  33194  prmidl0  33421  fldextrspunlsplem  33668  constrext2chnlem  33740  dya2icoseg  34268  omssubadd  34291  omsmeas  34314  oddpwdc  34345  logdivsqrle  34641  faclim  35733  faclim2  35735  taupilem1  37309  mblfinlem3  37653  mblfinlem4  37654  ibladdnclem  37670  iblmulc2nc  37679  abrexdom  37724  dalem3  39658  dalem8  39664  dalem25  39692  dalem27  39693  dalem38  39704  dalem44  39710  dalem54  39720  lhpat3  40040  4atexlemunv  40060  4atexlemtlw  40061  4atexlemc  40063  4atexlemnclw  40064  4atexlemex2  40065  4atexlemcnd  40066  cdleme0b  40206  cdleme0c  40207  cdleme0fN  40212  cdlemeulpq  40214  cdleme01N  40215  cdleme0ex1N  40217  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme3g  40228  cdleme3h  40229  cdleme4a  40233  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme9  40247  cdleme11fN  40258  cdleme11k  40262  cdleme15d  40271  cdlemednpq  40293  cdleme19c  40299  cdleme20aN  40303  cdleme20e  40307  cdleme21c  40321  cdleme21ct  40323  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme23a  40343  cdleme28a  40364  cdleme35f  40448  cdlemeg46frv  40519  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg6c  40614  cdlemg31a  40691  cdlemg31b  40692  cdlemk10  40837  cdlemk37  40908  dia2dimlem1  41058  dihjatcclem4  41415  imadomfi  41990  aks5lem1  42174  3cubeslem1  42672  irrapxlem3  42812  pell14qrgapw  42864  dgrsub2  43124  radcnvrat  44303  ressiooinf  45555  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  sumnnodd  45628  climlimsupcex  45767  cnrefiisplem  45827  stoweidlem1  45999  stoweidlem5  46003  stoweidlem7  46005  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem30  46135  fourierdlem42  46147  fourierdlem48  46152  fourierdlem62  46166  fourierdlem63  46167  fourierdlem68  46172  fourierdlem79  46183  sqwvfoura  46226  etransclem32  46264  hoidmvlelem2  46594  iunhoiioolem  46673  vonioolem1  46678  pimdecfgtioo  46715  pimincfltioo  46716  smfmullem1  46789  2ltceilhalf  47329  rehalfge1  47336  m1modnep2mod  47353  difmodm1lt  47360  fmtnoge3  47531  fmtnoprmfac2lem1  47567  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem4a  47609  proththdlem  47614  stgoldbwt  47777  sgoldbeven3prm  47784  mogoldbb  47786  evengpop3  47799  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  lindslinindimp2lem3  48449  fllogbd  48549  nnolog2flm1  48579