Theorem eqbrtrid 5130

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  map1  8973  xp1en  8987  map2xp  9071  rex2dom  9148  sucxpdom  9156  sniffsupp  9295  wdomima2g  9483  endjudisj  10071  dju1dif  10075  mapdjuen  10083  djuxpdom  10088  djufi  10089  pwsdompw  10105  infunsdom1  10114  infunsdom  10115  infxp  10116  ackbij1lem5  10125  hsmexlem4  10331  imadomg  10436  unidom  10445  unictb  10477  pwxpndom2  10567  pwdjundom  10569  distrnq  10863  nnne0  12170  supxrmnf  13223  xov1plusxeqvd  13405  quoremz  13766  quoremnn0ALT  13768  intfrac2  13769  m1modge3gt1  13832  bernneq2  14144  faclbnd4lem1  14207  01sqrexlem4  15159  reccn2  15511  caucvg  15593  o1fsum  15727  infcvgaux2i  15772  eirrlem  16120  rpnnen2lem12  16141  ruclem12  16157  nno  16300  divalglem5  16315  bitsfzolem  16352  bitsinv1lem  16359  bezoutlem3  16459  lcmfunsnlem  16559  coprmproddvds  16581  oddprmge3  16618  ge2nprmge4  16619  sqnprm  16620  prmreclem6  16840  4sqlem6  16862  4sqlem13  16876  4sqlem16  16879  4sqlem17  16880  2expltfac  17011  odcau  19524  sylow3  19553  efginvrel2  19647  lt6abl  19815  ablfac1lem  19990  gzrngunitlem  21378  zringlpirlem3  21410  dvdschrmulg  21474  znfld  21506  evlslem2  22025  chfacffsupp  22791  cpmidpmatlem3  22807  cctop  22941  csdfil  23829  xpsdsval  24316  nrginvrcnlem  24626  icccmplem2  24759  reconnlem2  24763  iscmet3lem3  25237  minveclem2  25373  minveclem4  25379  ivthlem2  25400  ivthlem3  25401  ovolunlem1a  25444  ovolfiniun  25449  ovoliunlem3  25452  ovoliun  25453  ovolicc2lem4  25468  unmbl  25485  ioombl1lem4  25509  itg2mono  25701  ibladdlem  25768  iblabsr  25778  iblmulc2  25779  bddiblnc  25790  dvferm1lem  25935  dvferm2lem  25937  lhop1lem  25965  dvcvx  25972  ftc1a  25991  plyeq0lem  26162  aannenlem3  26285  geolim3  26294  psercnlem1  26382  pserdvlem2  26385  reeff1olem  26403  pilem2  26409  pilem3  26410  cosq14gt0  26466  cosq14ge0  26467  cosne0  26485  recosf1o  26491  resinf1o  26492  argregt0  26566  logcnlem3  26600  logcnlem4  26601  logf1o2  26606  cxpcn3lem  26704  ang180lem2  26767  acosbnd  26857  atanbndlem  26882  leibpi  26899  cxp2lim  26934  emcllem2  26954  ftalem5  27034  basellem9  27046  vmage0  27078  chpge0  27083  chtub  27170  mersenne  27185  bposlem2  27243  bposlem5  27246  bposlem6  27247  bposlem9  27250  gausslemma2dlem0c  27316  gausslemma2dlem0e  27318  lgseisenlem1  27333  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  chebbnd1lem1  27427  chebbnd1lem2  27428  chebbnd1lem3  27429  mulog2sumlem2  27493  pntpbnd1a  27543  pntibndlem1  27547  pntibndlem3  27550  pntlemc  27553  ostth2  27595  ostth3  27596  absmuls  28202  pthdlem1  29765  numclwlk1lem2  30371  smcnlem  30698  minvecolem2  30876  minvecolem4  30881  strlem5  32256  hstrlem5  32264  abrexdomjm  32508  prct  32720  cyc3conja  33167  elrgspnlem2  33253  prmidl0  33459  mplvrpmga  33638  fldextrspunlsplem  33758  constrext2chnlem  33835  dya2icoseg  34362  omssubadd  34385  omsmeas  34408  oddpwdc  34439  logdivsqrle  34735  faclim  35862  faclim2  35864  taupilem1  37438  mblfinlem3  37772  mblfinlem4  37773  ibladdnclem  37789  iblmulc2nc  37798  abrexdom  37843  dalem3  39836  dalem8  39842  dalem25  39870  dalem27  39871  dalem38  39882  dalem44  39888  dalem54  39898  lhpat3  40218  4atexlemunv  40238  4atexlemtlw  40239  4atexlemc  40241  4atexlemnclw  40242  4atexlemex2  40243  4atexlemcnd  40244  cdleme0b  40384  cdleme0c  40385  cdleme0fN  40390  cdlemeulpq  40392  cdleme01N  40393  cdleme0ex1N  40395  cdleme2  40400  cdleme3b  40401  cdleme3c  40402  cdleme3g  40406  cdleme3h  40407  cdleme4a  40411  cdleme7aa  40414  cdleme7c  40417  cdleme7d  40418  cdleme7e  40419  cdleme9  40425  cdleme11fN  40436  cdleme11k  40440  cdleme15d  40449  cdlemednpq  40471  cdleme19c  40477  cdleme20aN  40481  cdleme20e  40485  cdleme21c  40499  cdleme21ct  40501  cdleme22e  40516  cdleme22eALTN  40517  cdleme22f  40518  cdleme23a  40521  cdleme28a  40542  cdleme35f  40626  cdlemeg46frv  40697  cdlemeg46rgv  40700  cdlemeg46req  40701  cdlemg2fv2  40772  cdlemg2m  40776  cdlemg6c  40792  cdlemg31a  40869  cdlemg31b  40870  cdlemk10  41015  cdlemk37  41086  dia2dimlem1  41236  dihjatcclem4  41593  imadomfi  42168  aks5lem1  42352  3cubeslem1  42841  irrapxlem3  42981  pell14qrgapw  43033  dgrsub2  43292  radcnvrat  44471  ressiooinf  45719  fmul01  45742  fmul01lt1lem1  45746  fmul01lt1lem2  45747  sumnnodd  45792  climlimsupcex  45929  cnrefiisplem  45989  stoweidlem1  46161  stoweidlem5  46165  stoweidlem7  46167  dirkercncflem1  46263  dirkercncflem4  46266  fourierdlem30  46297  fourierdlem42  46309  fourierdlem48  46314  fourierdlem62  46328  fourierdlem63  46329  fourierdlem68  46334  fourierdlem79  46345  sqwvfoura  46388  etransclem32  46426  hoidmvlelem2  46756  iunhoiioolem  46835  vonioolem1  46840  pimdecfgtioo  46877  pimincfltioo  46878  smfmullem1  46951  2ltceilhalf  47490  rehalfge1  47497  m1modnep2mod  47514  difmodm1lt  47521  fmtnoge3  47692  fmtnoprmfac2lem1  47728  sfprmdvdsmersenne  47765  lighneallem2  47768  lighneallem4a  47770  proththdlem  47775  stgoldbwt  47938  sgoldbeven3prm  47945  mogoldbb  47947  evengpop3  47960  bgoldbtbndlem2  47968  bgoldbtbndlem3  47969  lindslinindimp2lem3  48622  fllogbd  48722  nnolog2flm1  48752