Theorem eqbrtrid 5140

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 5139	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  map1  9047  xp1en  9061  map2xp  9145  rex2dom  9223  sucxpdom  9231  sniffsupp  9370  wdomima2g  9558  endjudisj  10171  dju1dif  10175  mapdjuen  10183  djuxpdom  10188  djufi  10189  pwsdompw  10205  infunsdom1  10214  infunsdom  10215  infxp  10216  ackbij1lem5  10225  hsmexlem4  10431  imadomg  10537  imadomnum  10538  unidom  10551  unictb  10584  pwxpndom2  10674  pwdjundom  10676  distrnq  10970  nnne0  12294  supxrmnf  13369  xov1plusxeqvd  13551  quoremz  13916  quoremnn0ALT  13918  intfrac2  13919  m1modge3gt1  13982  bernneq2  14294  faclbnd4lem1  14357  01sqrexlem4  15332  reccn2  15684  caucvg  15766  o1fsum  15900  infcvgaux2i  15947  eirrlem  16292  rpnnen2lem12  16313  ruclem12  16329  nno  16472  divalglem5  16487  bitsfzolem  16524  bitsinv1lem  16531  bezoutlem3  16631  lcmfunsnlem  16731  coprmproddvds  16753  oddprmge3  16791  ge2nprmge4  16792  sqnprm  16793  prmreclem6  17013  4sqlem6  17035  4sqlem13  17049  4sqlem16  17052  4sqlem17  17053  2expltfac  17184  odcau  19731  sylow3  19760  efginvrel2  19854  lt6abl  20022  ablfac1lem  20197  prmidl0  21541  gzrngunitlem  21645  zringlpirlem3  21677  dvdschrmulg  21741  znfld  21773  evlslem2  22295  chfacffsupp  23081  cpmidpmatlem3  23097  cctop  23231  csdfil  24120  xpsdsval  24607  nrginvrcnlem  24917  icccmplem2  25050  reconnlem2  25054  iscmet3lem3  25518  minveclem2  25654  minveclem4  25660  ivthlem2  25680  ivthlem3  25681  ovolunlem1a  25724  ovolfiniun  25729  ovoliunlem3  25732  ovoliun  25733  ovolicc2lem4  25748  unmbl  25765  ioombl1lem4  25789  itg2mono  25981  ibladdlem  26047  iblabsr  26057  iblmulc2  26058  bddiblnc  26069  dvferm1lem  26211  dvferm2lem  26213  lhop1lem  26240  dvcvx  26247  ftc1a  26264  plyeq0lem  26436  aannenlem3  26566  geolim3  26575  psercnlem1  26661  pserdvlem2  26664  reeff1olem  26682  pilem2  26688  pilem3  26689  cosq14gt0  26748  cosq14ge0  26749  cosne0  26766  recosf1o  26772  resinf1o  26773  argregt0  26847  logcnlem3  26881  logcnlem4  26882  logf1o2  26887  cxpcn3lem  26984  ang180lem2  27047  acosbnd  27137  atanbndlem  27162  leibpi  27179  cxp2lim  27213  emcllem2  27233  ftalem5  27313  basellem9  27325  vmage0  27357  chpge0  27362  chtub  27448  mersenne  27463  bposlem2  27521  bposlem5  27524  bposlem6  27525  bposlem9  27528  gausslemma2dlem0c  27594  gausslemma2dlem0e  27596  lgseisenlem1  27611  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  chebbnd1lem1  27705  chebbnd1lem2  27706  chebbnd1lem3  27707  mulog2sumlem2  27771  pntpbnd1a  27821  pntibndlem1  27825  pntibndlem3  27828  pntlemc  27831  ostth2  27873  ostth3  27874  absmuls  28509  pthdlem1  30231  numclwlk1lem2  30850  smcnlem  31178  minvecolem2  31356  minvecolem4  31361  strlem5  32736  hstrlem5  32744  abrexdomjm  32982  prct  33185  cyc3conja  33597  elrgspnlem2  33683  mplvrpmga  34055  psrmonprod  34062  fldextrspunlsplem  34183  constrext2chnlem  34260  dya2icoseg  34788  omssubadd  34811  omsmeas  34834  oddpwdc  34865  logdivsqrle  35158  faclim  36325  faclim2  36327  taupilem1  38073  mblfinlem3  38408  mblfinlem4  38409  ibladdnclem  38425  iblmulc2nc  38434  abrexdom  38480  dalem3  40537  dalem8  40543  dalem25  40571  dalem27  40572  dalem38  40583  dalem44  40589  dalem54  40599  lhpat3  40919  4atexlemunv  40939  4atexlemtlw  40940  4atexlemc  40942  4atexlemnclw  40943  4atexlemex2  40944  4atexlemcnd  40945  cdleme0b  41085  cdleme0c  41086  cdleme0fN  41091  cdlemeulpq  41093  cdleme01N  41094  cdleme0ex1N  41096  cdleme2  41101  cdleme3b  41102  cdleme3c  41103  cdleme3g  41107  cdleme3h  41108  cdleme4a  41112  cdleme7aa  41115  cdleme7c  41118  cdleme7d  41119  cdleme7e  41120  cdleme9  41126  cdleme11fN  41137  cdleme11k  41141  cdleme15d  41150  cdlemednpq  41172  cdleme19c  41178  cdleme20aN  41182  cdleme20e  41186  cdleme21c  41200  cdleme21ct  41202  cdleme22e  41217  cdleme22eALTN  41218  cdleme22f  41219  cdleme23a  41222  cdleme28a  41243  cdleme35f  41327  cdlemeg46frv  41398  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemg2fv2  41473  cdlemg2m  41477  cdlemg6c  41493  cdlemg31a  41570  cdlemg31b  41571  cdlemk10  41716  cdlemk37  41787  dia2dimlem1  41937  dihjatcclem4  42294  imadomfi  42868  aks5lem1  43052  3cubeslem1  43529  irrapxlem3  43665  pell14qrgapw  43717  dgrsub2  43976  radcnvrat  45138  ressiooinf  46387  fmul01  46410  fmul01lt1lem1  46414  fmul01lt1lem2  46415  sumnnodd  46460  climlimsupcex  46597  cnrefiisplem  46657  stoweidlem1  46829  stoweidlem5  46833  stoweidlem7  46835  dirkercncflem1  46931  dirkercncflem4  46934  fourierdlem30  46965  fourierdlem42  46977  fourierdlem48  46982  fourierdlem49  46983  fourierdlem62  46996  fourierdlem63  46997  fourierdlem68  47002  fourierdlem79  47013  sqwvfoura  47056  etransclem32  47094  hoidmvlelem2  47424  iunhoiioolem  47503  vonioolem1  47508  pimdecfgtioo  47545  pimincfltioo  47546  smfmullem1  47619  2ltceilhalf  48220  rehalfge1  48227  m1modnep2mod  48246  difmodm1lt  48253  2timesltsqm1  48267  fmtnoge3  48433  fmtnoprmfac2lem1  48469  sfprmdvdsmersenne  48506  lighneallem2  48509  lighneallem4a  48511  proththdlem  48516  nprmdvdsfacm1lem2  48524  stgoldbwt  48692  sgoldbeven3prm  48699  mogoldbb  48701  evengpop3  48714  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  lindslinindimp2lem3  49390  fllogbd  49490  nnolog2flm1  49520