Theorem eqbrtrid 5139

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  map1  9069  xp1en  9083  map2xp  9167  rex2dom  9245  sucxpdom  9253  sniffsupp  9393  wdomima2g  9581  endjudisj  10248  dju1dif  10252  mapdjuen  10260  djuxpdom  10265  djufi  10266  pwsdompw  10282  infunsdom1  10291  infunsdom  10292  infxp  10293  ackbij1lem5  10302  hsmexlem4  10508  imadomg  10614  imadomnum  10615  unidom  10628  unictb  10661  pwxpndom2  10751  pwdjundom  10753  distrnq  11047  nnne0  12373  supxrmnf  13448  xov1plusxeqvd  13630  quoremz  13996  quoremnn0ALT  13998  intfrac2  13999  m1modge3gt1  14062  bernneq2  14375  faclbnd4lem1  14438  01sqrexlem4  15413  reccn2  15765  caucvg  15847  o1fsum  15981  infcvgaux2i  16028  eirrlem  16373  rpnnen2lem12  16394  ruclem12  16410  nno  16553  divalglem5  16568  bitsfzolem  16605  bitsinv1lem  16612  bezoutlem3  16715  lcmfunsnlem  16817  coprmproddvds  16839  oddprmge3  16877  ge2nprmge4  16878  sqnprm  16879  prmreclem6  17100  4sqlem6  17122  4sqlem13  17136  4sqlem16  17139  4sqlem17  17140  2expltfac  17271  odcau  19819  sylow3  19848  efginvrel2  19942  lt6abl  20110  ablfac1lem  20285  prmidl0  21635  gzrngunitlem  21739  zringlpirlem3  21771  dvdschrmulg  21835  znfld  21867  evlslem2  22389  chfacffsupp  23175  cpmidpmatlem3  23191  cctop  23325  csdfil  24214  xpsdsval  24701  nrginvrcnlem  25011  icccmplem2  25144  reconnlem2  25148  iscmet3lem3  25612  minveclem2  25748  minveclem4  25754  ivthlem2  25774  ivthlem3  25775  ovolunlem1a  25818  ovolfiniun  25823  ovoliunlem3  25826  ovoliun  25827  ovolicc2lem4  25842  unmbl  25859  ioombl1lem4  25883  itg2mono  26075  ibladdlem  26141  iblabsr  26151  iblmulc2  26152  bddiblnc  26163  dvferm1lem  26305  dvferm2lem  26307  lhop1lem  26334  dvcvx  26341  ftc1a  26358  plyeq0lem  26530  aannenlem3  26658  geolim3  26667  psercnlem1  26753  pserdvlem2  26756  reeff1olem  26774  pilem2  26780  pilem3  26781  cosq14gt0  26840  cosq14ge0  26841  cosne0  26858  recosf1o  26864  resinf1o  26865  argregt0  26939  logcnlem3  26973  logcnlem4  26974  logf1o2  26979  cxpcn3lem  27076  ang180lem2  27139  acosbnd  27229  atanbndlem  27254  leibpi  27271  cxp2lim  27305  emcllem2  27325  ftalem5  27405  basellem9  27417  vmage0  27449  chpge0  27454  chtub  27540  mersenne  27555  bposlem2  27613  bposlem5  27616  bposlem6  27617  bposlem9  27620  gausslemma2dlem0c  27686  gausslemma2dlem0e  27688  lgseisenlem1  27703  lgsquadlem1  27708  lgsquadlem2  27709  lgsquadlem3  27710  chebbnd1lem1  27797  chebbnd1lem2  27798  chebbnd1lem3  27799  mulog2sumlem2  27863  pntpbnd1a  27913  pntibndlem1  27917  pntibndlem3  27920  pntlemc  27923  ostth2  27965  ostth3  27966  fltoprmlem2  27995  absmuls  28631  pthdlem1  30353  numclwlk1lem2  30972  smcnlem  31300  minvecolem2  31478  minvecolem4  31483  strlem5  32858  hstrlem5  32866  abrexdomjm  33146  prct  33349  cyc3conja  33761  elrgspnlem2  33847  mplvrpmga  34220  psrmonprod  34227  fldextrspunlsplem  34348  constrext2chnlem  34425  dya2icoseg  34952  omssubadd  34975  omsmeas  34998  oddpwdc  35029  logdivsqrle  35322  faclim  36586  faclim2  36588  taupilem1  38318  mblfinlem3  38653  mblfinlem4  38654  ibladdnclem  38670  iblmulc2nc  38679  abrexdom  38740  dalem3  40797  dalem8  40803  dalem25  40831  dalem27  40832  dalem38  40843  dalem44  40849  dalem54  40859  lhpat3  41179  4atexlemunv  41199  4atexlemtlw  41200  4atexlemc  41202  4atexlemnclw  41203  4atexlemex2  41204  4atexlemcnd  41205  cdleme0b  41345  cdleme0c  41346  cdleme0fN  41351  cdlemeulpq  41353  cdleme01N  41354  cdleme0ex1N  41356  cdleme2  41361  cdleme3b  41362  cdleme3c  41363  cdleme3g  41367  cdleme3h  41368  cdleme4a  41372  cdleme7aa  41375  cdleme7c  41378  cdleme7d  41379  cdleme7e  41380  cdleme9  41386  cdleme11fN  41397  cdleme11k  41401  cdleme15d  41410  cdlemednpq  41432  cdleme19c  41438  cdleme20aN  41442  cdleme20e  41446  cdleme21c  41460  cdleme21ct  41462  cdleme22e  41477  cdleme22eALTN  41478  cdleme22f  41479  cdleme23a  41482  cdleme28a  41503  cdleme35f  41587  cdlemeg46frv  41658  cdlemeg46rgv  41661  cdlemeg46req  41662  cdlemg2fv2  41733  cdlemg2m  41737  cdlemg6c  41753  cdlemg31a  41830  cdlemg31b  41831  cdlemk10  41976  cdlemk37  42047  dia2dimlem1  42197  dihjatcclem4  42554  imadomfi  43128  aks5lem1  43312  3cubeslem1  43770  irrapxlem3  43907  pell14qrgapw  43959  dgrsub2  44213  radcnvrat  45374  ressiooinf  46645  fmul01  46668  fmul01lt1lem1  46672  fmul01lt1lem2  46673  sumnnodd  46718  climlimsupcex  46855  cnrefiisplem  46915  stoweidlem1  47087  stoweidlem5  47091  stoweidlem7  47093  dirkercncflem1  47189  dirkercncflem4  47192  fourierdlem30  47223  fourierdlem42  47235  fourierdlem48  47240  fourierdlem49  47241  fourierdlem62  47254  fourierdlem63  47255  fourierdlem68  47260  fourierdlem79  47271  sqwvfoura  47314  etransclem32  47352  hoidmvlelem2  47682  iunhoiioolem  47761  vonioolem1  47766  pimdecfgtioo  47803  pimincfltioo  47804  smfmullem1  47877  2ltceilhalf  48478  rehalfge1  48485  m1modnep2mod  48504  difmodm1lt  48511  2timesltsqm1  48525  fmtnoge3  48691  fmtnoprmfac2lem1  48727  sfprmdvdsmersenne  48764  lighneallem2  48767  lighneallem4a  48769  proththdlem  48774  nprmdvdsfacm1lem2  48782  stgoldbwt  48950  sgoldbeven3prm  48957  mogoldbb  48959  evengpop3  48972  bgoldbtbndlem2  48980  bgoldbtbndlem3  48981  lindslinindimp2lem3  49648  fllogbd  49748  nnolog2flm1  49778