Theorem eqbrtrid 5126

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5091

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092

This theorem is referenced by:  map1  8962  xp1en  8976  map2xp  9060  rex2dom  9137  sucxpdom  9145  sniffsupp  9284  wdomima2g  9472  endjudisj  10060  dju1dif  10064  mapdjuen  10072  djuxpdom  10077  djufi  10078  pwsdompw  10094  infunsdom1  10103  infunsdom  10104  infxp  10105  ackbij1lem5  10114  hsmexlem4  10320  imadomg  10425  unidom  10434  unictb  10466  pwxpndom2  10556  pwdjundom  10558  distrnq  10852  nnne0  12159  supxrmnf  13216  xov1plusxeqvd  13398  quoremz  13759  quoremnn0ALT  13761  intfrac2  13762  m1modge3gt1  13825  bernneq2  14137  faclbnd4lem1  14200  01sqrexlem4  15152  reccn2  15504  caucvg  15586  o1fsum  15720  infcvgaux2i  15765  eirrlem  16113  rpnnen2lem12  16134  ruclem12  16150  nno  16293  divalglem5  16308  bitsfzolem  16345  bitsinv1lem  16352  bezoutlem3  16452  lcmfunsnlem  16552  coprmproddvds  16574  oddprmge3  16611  ge2nprmge4  16612  sqnprm  16613  prmreclem6  16833  4sqlem6  16855  4sqlem13  16869  4sqlem16  16872  4sqlem17  16873  2expltfac  17004  odcau  19517  sylow3  19546  efginvrel2  19640  lt6abl  19808  ablfac1lem  19983  gzrngunitlem  21370  zringlpirlem3  21402  dvdschrmulg  21466  znfld  21498  evlslem2  22015  chfacffsupp  22772  cpmidpmatlem3  22788  cctop  22922  csdfil  23810  xpsdsval  24297  nrginvrcnlem  24607  icccmplem2  24740  reconnlem2  24744  iscmet3lem3  25218  minveclem2  25354  minveclem4  25360  ivthlem2  25381  ivthlem3  25382  ovolunlem1a  25425  ovolfiniun  25430  ovoliunlem3  25433  ovoliun  25434  ovolicc2lem4  25449  unmbl  25466  ioombl1lem4  25490  itg2mono  25682  ibladdlem  25749  iblabsr  25759  iblmulc2  25760  bddiblnc  25771  dvferm1lem  25916  dvferm2lem  25918  lhop1lem  25946  dvcvx  25953  ftc1a  25972  plyeq0lem  26143  aannenlem3  26266  geolim3  26275  psercnlem1  26363  pserdvlem2  26366  reeff1olem  26384  pilem2  26390  pilem3  26391  cosq14gt0  26447  cosq14ge0  26448  cosne0  26466  recosf1o  26472  resinf1o  26473  argregt0  26547  logcnlem3  26581  logcnlem4  26582  logf1o2  26587  cxpcn3lem  26685  ang180lem2  26748  acosbnd  26838  atanbndlem  26863  leibpi  26880  cxp2lim  26915  emcllem2  26935  ftalem5  27015  basellem9  27027  vmage0  27059  chpge0  27064  chtub  27151  mersenne  27166  bposlem2  27224  bposlem5  27227  bposlem6  27228  bposlem9  27231  gausslemma2dlem0c  27297  gausslemma2dlem0e  27299  lgseisenlem1  27314  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  mulog2sumlem2  27474  pntpbnd1a  27524  pntibndlem1  27528  pntibndlem3  27531  pntlemc  27534  ostth2  27576  ostth3  27577  absmuls  28183  pthdlem1  29745  numclwlk1lem2  30348  smcnlem  30675  minvecolem2  30853  minvecolem4  30858  strlem5  32233  hstrlem5  32241  abrexdomjm  32485  prct  32694  cyc3conja  33124  elrgspnlem2  33208  prmidl0  33413  mplvrpmga  33573  fldextrspunlsplem  33684  constrext2chnlem  33761  dya2icoseg  34288  omssubadd  34311  omsmeas  34334  oddpwdc  34365  logdivsqrle  34661  faclim  35788  faclim2  35790  taupilem1  37361  mblfinlem3  37705  mblfinlem4  37706  ibladdnclem  37722  iblmulc2nc  37731  abrexdom  37776  dalem3  39709  dalem8  39715  dalem25  39743  dalem27  39744  dalem38  39755  dalem44  39761  dalem54  39771  lhpat3  40091  4atexlemunv  40111  4atexlemtlw  40112  4atexlemc  40114  4atexlemnclw  40115  4atexlemex2  40116  4atexlemcnd  40117  cdleme0b  40257  cdleme0c  40258  cdleme0fN  40263  cdlemeulpq  40265  cdleme01N  40266  cdleme0ex1N  40268  cdleme2  40273  cdleme3b  40274  cdleme3c  40275  cdleme3g  40279  cdleme3h  40280  cdleme4a  40284  cdleme7aa  40287  cdleme7c  40290  cdleme7d  40291  cdleme7e  40292  cdleme9  40298  cdleme11fN  40309  cdleme11k  40313  cdleme15d  40322  cdlemednpq  40344  cdleme19c  40350  cdleme20aN  40354  cdleme20e  40358  cdleme21c  40372  cdleme21ct  40374  cdleme22e  40389  cdleme22eALTN  40390  cdleme22f  40391  cdleme23a  40394  cdleme28a  40415  cdleme35f  40499  cdlemeg46frv  40570  cdlemeg46rgv  40573  cdlemeg46req  40574  cdlemg2fv2  40645  cdlemg2m  40649  cdlemg6c  40665  cdlemg31a  40742  cdlemg31b  40743  cdlemk10  40888  cdlemk37  40959  dia2dimlem1  41109  dihjatcclem4  41466  imadomfi  42041  aks5lem1  42225  3cubeslem1  42723  irrapxlem3  42863  pell14qrgapw  42915  dgrsub2  43174  radcnvrat  44353  ressiooinf  45603  fmul01  45626  fmul01lt1lem1  45630  fmul01lt1lem2  45631  sumnnodd  45676  climlimsupcex  45813  cnrefiisplem  45873  stoweidlem1  46045  stoweidlem5  46049  stoweidlem7  46051  dirkercncflem1  46147  dirkercncflem4  46150  fourierdlem30  46181  fourierdlem42  46193  fourierdlem48  46198  fourierdlem62  46212  fourierdlem63  46213  fourierdlem68  46218  fourierdlem79  46229  sqwvfoura  46272  etransclem32  46310  hoidmvlelem2  46640  iunhoiioolem  46719  vonioolem1  46724  pimdecfgtioo  46761  pimincfltioo  46762  smfmullem1  46835  2ltceilhalf  47365  rehalfge1  47372  m1modnep2mod  47389  difmodm1lt  47396  fmtnoge3  47567  fmtnoprmfac2lem1  47603  sfprmdvdsmersenne  47640  lighneallem2  47643  lighneallem4a  47645  proththdlem  47650  stgoldbwt  47813  sgoldbeven3prm  47820  mogoldbb  47822  evengpop3  47835  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  lindslinindimp2lem3  48498  fllogbd  48598  nnolog2flm1  48628