Theorem eqbrtrid 5110

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  map1  8839  xp1en  8853  map2xp  8943  1sdom  9034  sucxpdom  9041  sniffsupp  9168  wdomima2g  9354  endjudisj  9933  dju1dif  9937  mapdjuen  9945  djuxpdom  9950  djufi  9951  pwsdompw  9969  infunsdom1  9978  infunsdom  9979  infxp  9980  ackbij1lem5  9989  hsmexlem4  10194  imadomg  10299  unidom  10308  unictb  10340  pwxpndom2  10430  pwdjundom  10432  distrnq  10726  nnne0  12016  supxrmnf  13060  xov1plusxeqvd  13239  quoremz  13584  quoremnn0ALT  13586  intfrac2  13587  m1modge3gt1  13647  bernneq2  13954  faclbnd4lem1  14016  sqrlem4  14966  reccn2  15315  caucvg  15399  o1fsum  15534  infcvgaux2i  15579  eirrlem  15922  rpnnen2lem12  15943  ruclem12  15959  nno  16100  divalglem5  16115  bitsfzolem  16150  bitsinv1lem  16157  bezoutlem3  16258  lcmfunsnlem  16355  coprmproddvds  16377  oddprmge3  16414  ge2nprmge4  16415  sqnprm  16416  prmreclem6  16631  4sqlem6  16653  4sqlem13  16667  4sqlem16  16670  4sqlem17  16671  2expltfac  16803  odcau  19218  sylow3  19247  efginvrel2  19342  lt6abl  19505  ablfac1lem  19680  gzrngunitlem  20672  zringlpirlem3  20695  znfld  20777  evlslem2  21298  chfacffsupp  22014  cpmidpmatlem3  22030  cctop  22165  csdfil  23054  xpsdsval  23543  nrginvrcnlem  23864  icccmplem2  23995  reconnlem2  23999  iscmet3lem3  24463  minveclem2  24599  minveclem4  24605  ivthlem2  24625  ivthlem3  24626  ovolunlem1a  24669  ovolfiniun  24674  ovoliunlem3  24677  ovoliun  24678  ovolicc2lem4  24693  unmbl  24710  ioombl1lem4  24734  itg2mono  24927  ibladdlem  24993  iblabsr  25003  iblmulc2  25004  bddiblnc  25015  dvferm1lem  25157  dvferm2lem  25159  lhop1lem  25186  dvcvx  25193  ftc1a  25210  plyeq0lem  25380  aannenlem3  25499  geolim3  25508  psercnlem1  25593  pserdvlem2  25596  reeff1olem  25614  pilem2  25620  pilem3  25621  cosq14gt0  25676  cosq14ge0  25677  cosne0  25694  recosf1o  25700  resinf1o  25701  argregt0  25774  logcnlem3  25808  logcnlem4  25809  logf1o2  25814  cxpcn3lem  25909  ang180lem2  25969  acosbnd  26059  atanbndlem  26084  leibpi  26101  cxp2lim  26135  emcllem2  26155  ftalem5  26235  basellem9  26247  vmage0  26279  chpge0  26284  chtub  26369  mersenne  26384  bposlem2  26442  bposlem5  26445  bposlem6  26446  bposlem9  26449  gausslemma2dlem0c  26515  gausslemma2dlem0e  26517  lgseisenlem1  26532  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  chebbnd1lem1  26626  chebbnd1lem2  26627  chebbnd1lem3  26628  mulog2sumlem2  26692  pntpbnd1a  26742  pntibndlem1  26746  pntibndlem3  26749  pntlemc  26752  ostth2  26794  ostth3  26795  pthdlem1  28143  numclwlk1lem2  28743  smcnlem  29068  minvecolem2  29246  minvecolem4  29251  strlem5  30626  hstrlem5  30634  abrexdomjm  30861  prct  31058  cyc3conja  31433  dvdschrmulg  31492  prmidl0  31635  dya2icoseg  32253  omssubadd  32276  omsmeas  32299  oddpwdc  32330  logdivsqrle  32639  faclim  33721  faclim2  33723  taupilem1  35501  mblfinlem3  35825  mblfinlem4  35826  ibladdnclem  35842  iblmulc2nc  35851  abrexdom  35897  dalem3  37685  dalem8  37691  dalem25  37719  dalem27  37720  dalem38  37731  dalem44  37737  dalem54  37747  lhpat3  38067  4atexlemunv  38087  4atexlemtlw  38088  4atexlemc  38090  4atexlemnclw  38091  4atexlemex2  38092  4atexlemcnd  38093  cdleme0b  38233  cdleme0c  38234  cdleme0fN  38239  cdlemeulpq  38241  cdleme01N  38242  cdleme0ex1N  38244  cdleme2  38249  cdleme3b  38250  cdleme3c  38251  cdleme3g  38255  cdleme3h  38256  cdleme4a  38260  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme9  38274  cdleme11fN  38285  cdleme11k  38289  cdleme15d  38298  cdlemednpq  38320  cdleme19c  38326  cdleme20aN  38330  cdleme20e  38334  cdleme21c  38348  cdleme21ct  38350  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f  38367  cdleme23a  38370  cdleme28a  38391  cdleme35f  38475  cdlemeg46frv  38546  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemg2fv2  38621  cdlemg2m  38625  cdlemg6c  38641  cdlemg31a  38718  cdlemg31b  38719  cdlemk10  38864  cdlemk37  38935  dia2dimlem1  39085  dihjatcclem4  39442  metakunt30  40161  3cubeslem1  40513  irrapxlem3  40653  pell14qrgapw  40705  dgrsub2  40967  radcnvrat  41939  ressiooinf  43102  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  sumnnodd  43178  climlimsupcex  43317  cnrefiisplem  43377  stoweidlem1  43549  stoweidlem5  43553  stoweidlem7  43555  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem30  43685  fourierdlem42  43697  fourierdlem48  43702  fourierdlem62  43716  fourierdlem63  43717  fourierdlem68  43722  fourierdlem79  43733  sqwvfoura  43776  etransclem32  43814  hoidmvlelem2  44141  iunhoiioolem  44220  vonioolem1  44225  pimdecfgtioo  44262  pimincfltioo  44263  smfmullem1  44336  fmtnoge3  44993  fmtnoprmfac2lem1  45029  sfprmdvdsmersenne  45066  lighneallem2  45069  lighneallem4a  45071  proththdlem  45076  stgoldbwt  45239  sgoldbeven3prm  45246  mogoldbb  45248  evengpop3  45261  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  lindslinindimp2lem3  45812  fllogbd  45917  nnolog2flm1  45947