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 2761	. 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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  9061  xp1en  9075  map2xp  9159  rex2dom  9237  sucxpdom  9245  sniffsupp  9385  wdomima2g  9573  endjudisj  10240  dju1dif  10244  mapdjuen  10252  djuxpdom  10257  djufi  10258  pwsdompw  10274  infunsdom1  10283  infunsdom  10284  infxp  10285  ackbij1lem5  10294  hsmexlem4  10500  imadomg  10606  imadomnum  10607  unidom  10620  unictb  10653  pwxpndom2  10743  pwdjundom  10745  distrnq  11039  nnne0  12365  supxrmnf  13440  xov1plusxeqvd  13622  quoremz  13988  quoremnn0ALT  13990  intfrac2  13991  m1modge3gt1  14054  bernneq2  14367  faclbnd4lem1  14430  01sqrexlem4  15405  reccn2  15757  caucvg  15839  o1fsum  15973  infcvgaux2i  16020  eirrlem  16365  rpnnen2lem12  16386  ruclem12  16402  nno  16545  divalglem5  16560  bitsfzolem  16597  bitsinv1lem  16604  bezoutlem3  16707  lcmfunsnlem  16809  coprmproddvds  16831  oddprmge3  16869  ge2nprmge4  16870  sqnprm  16871  prmreclem6  17092  4sqlem6  17114  4sqlem13  17128  4sqlem16  17131  4sqlem17  17132  2expltfac  17263  odcau  19811  sylow3  19840  efginvrel2  19934  lt6abl  20102  ablfac1lem  20277  prmidl0  21627  gzrngunitlem  21731  zringlpirlem3  21763  dvdschrmulg  21827  znfld  21859  evlslem2  22381  chfacffsupp  23167  cpmidpmatlem3  23183  cctop  23317  csdfil  24206  xpsdsval  24693  nrginvrcnlem  25003  icccmplem2  25136  reconnlem2  25140  iscmet3lem3  25604  minveclem2  25740  minveclem4  25746  ivthlem2  25766  ivthlem3  25767  ovolunlem1a  25810  ovolfiniun  25815  ovoliunlem3  25818  ovoliun  25819  ovolicc2lem4  25834  unmbl  25851  ioombl1lem4  25875  itg2mono  26067  ibladdlem  26133  iblabsr  26143  iblmulc2  26144  bddiblnc  26155  dvferm1lem  26297  dvferm2lem  26299  lhop1lem  26326  dvcvx  26333  ftc1a  26350  plyeq0lem  26522  aannenlem3  26650  geolim3  26659  psercnlem1  26745  pserdvlem2  26748  reeff1olem  26766  pilem2  26772  pilem3  26773  cosq14gt0  26832  cosq14ge0  26833  cosne0  26850  recosf1o  26856  resinf1o  26857  argregt0  26931  logcnlem3  26965  logcnlem4  26966  logf1o2  26971  cxpcn3lem  27068  ang180lem2  27131  acosbnd  27221  atanbndlem  27246  leibpi  27263  cxp2lim  27297  emcllem2  27317  ftalem5  27397  basellem9  27409  vmage0  27441  chpge0  27446  chtub  27532  mersenne  27547  bposlem2  27605  bposlem5  27608  bposlem6  27609  bposlem9  27612  gausslemma2dlem0c  27678  gausslemma2dlem0e  27680  lgseisenlem1  27695  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  chebbnd1lem1  27789  chebbnd1lem2  27790  chebbnd1lem3  27791  mulog2sumlem2  27855  pntpbnd1a  27905  pntibndlem1  27909  pntibndlem3  27912  pntlemc  27915  ostth2  27957  ostth3  27958  fltoprmlem2  27987  absmuls  28623  pthdlem1  30345  numclwlk1lem2  30964  smcnlem  31292  minvecolem2  31470  minvecolem4  31475  strlem5  32850  hstrlem5  32858  abrexdomjm  33096  prct  33299  cyc3conja  33711  elrgspnlem2  33797  mplvrpmga  34170  psrmonprod  34177  fldextrspunlsplem  34298  constrext2chnlem  34375  dya2icoseg  34902  omssubadd  34925  omsmeas  34948  oddpwdc  34979  logdivsqrle  35272  faclim  36490  faclim2  36492  taupilem1  38222  mblfinlem3  38557  mblfinlem4  38558  ibladdnclem  38574  iblmulc2nc  38583  abrexdom  38644  dalem3  40701  dalem8  40707  dalem25  40735  dalem27  40736  dalem38  40747  dalem44  40753  dalem54  40763  lhpat3  41083  4atexlemunv  41103  4atexlemtlw  41104  4atexlemc  41106  4atexlemnclw  41107  4atexlemex2  41108  4atexlemcnd  41109  cdleme0b  41249  cdleme0c  41250  cdleme0fN  41255  cdlemeulpq  41257  cdleme01N  41258  cdleme0ex1N  41260  cdleme2  41265  cdleme3b  41266  cdleme3c  41267  cdleme3g  41271  cdleme3h  41272  cdleme4a  41276  cdleme7aa  41279  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme9  41290  cdleme11fN  41301  cdleme11k  41305  cdleme15d  41314  cdlemednpq  41336  cdleme19c  41342  cdleme20aN  41346  cdleme20e  41350  cdleme21c  41364  cdleme21ct  41366  cdleme22e  41381  cdleme22eALTN  41382  cdleme22f  41383  cdleme23a  41386  cdleme28a  41407  cdleme35f  41491  cdlemeg46frv  41562  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemg2fv2  41637  cdlemg2m  41641  cdlemg6c  41657  cdlemg31a  41734  cdlemg31b  41735  cdlemk10  41880  cdlemk37  41951  dia2dimlem1  42101  dihjatcclem4  42458  imadomfi  43032  aks5lem1  43216  3cubeslem1  43674  irrapxlem3  43810  pell14qrgapw  43862  dgrsub2  44121  radcnvrat  45283  ressiooinf  46538  fmul01  46561  fmul01lt1lem1  46565  fmul01lt1lem2  46566  sumnnodd  46611  climlimsupcex  46748  cnrefiisplem  46808  stoweidlem1  46980  stoweidlem5  46984  stoweidlem7  46986  dirkercncflem1  47082  dirkercncflem4  47085  fourierdlem30  47116  fourierdlem42  47128  fourierdlem48  47133  fourierdlem49  47134  fourierdlem62  47147  fourierdlem63  47148  fourierdlem68  47153  fourierdlem79  47164  sqwvfoura  47207  etransclem32  47245  hoidmvlelem2  47575  iunhoiioolem  47654  vonioolem1  47659  pimdecfgtioo  47696  pimincfltioo  47697  smfmullem1  47770  2ltceilhalf  48371  rehalfge1  48378  m1modnep2mod  48397  difmodm1lt  48404  2timesltsqm1  48418  fmtnoge3  48584  fmtnoprmfac2lem1  48620  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem4a  48662  proththdlem  48667  nprmdvdsfacm1lem2  48675  stgoldbwt  48843  sgoldbeven3prm  48850  mogoldbb  48852  evengpop3  48865  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  lindslinindimp2lem3  49541  fllogbd  49641  nnolog2flm1  49671