Theorem eqbrtrid 5158

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124

This theorem is referenced by:  map1  9062  xp1en  9079  map2xp  9169  rex2dom  9264  1sdomOLD  9267  sucxpdom  9273  sniffsupp  9422  wdomima2g  9608  endjudisj  10191  dju1dif  10195  mapdjuen  10203  djuxpdom  10208  djufi  10209  pwsdompw  10225  infunsdom1  10234  infunsdom  10235  infxp  10236  ackbij1lem5  10245  hsmexlem4  10451  imadomg  10556  unidom  10565  unictb  10597  pwxpndom2  10687  pwdjundom  10689  distrnq  10983  nnne0  12282  supxrmnf  13341  xov1plusxeqvd  13520  quoremz  13877  quoremnn0ALT  13879  intfrac2  13880  m1modge3gt1  13941  bernneq2  14251  faclbnd4lem1  14314  01sqrexlem4  15266  reccn2  15615  caucvg  15697  o1fsum  15831  infcvgaux2i  15876  eirrlem  16222  rpnnen2lem12  16243  ruclem12  16259  nno  16401  divalglem5  16416  bitsfzolem  16453  bitsinv1lem  16460  bezoutlem3  16560  lcmfunsnlem  16660  coprmproddvds  16682  oddprmge3  16719  ge2nprmge4  16720  sqnprm  16721  prmreclem6  16941  4sqlem6  16963  4sqlem13  16977  4sqlem16  16980  4sqlem17  16981  2expltfac  17112  odcau  19590  sylow3  19619  efginvrel2  19713  lt6abl  19881  ablfac1lem  20056  gzrngunitlem  21412  zringlpirlem3  21437  dvdschrmulg  21501  znfld  21533  evlslem2  22051  chfacffsupp  22810  cpmidpmatlem3  22826  cctop  22960  csdfil  23848  xpsdsval  24336  nrginvrcnlem  24648  icccmplem2  24781  reconnlem2  24785  iscmet3lem3  25260  minveclem2  25396  minveclem4  25402  ivthlem2  25423  ivthlem3  25424  ovolunlem1a  25467  ovolfiniun  25472  ovoliunlem3  25475  ovoliun  25476  ovolicc2lem4  25491  unmbl  25508  ioombl1lem4  25532  itg2mono  25724  ibladdlem  25791  iblabsr  25801  iblmulc2  25802  bddiblnc  25813  dvferm1lem  25958  dvferm2lem  25960  lhop1lem  25988  dvcvx  25995  ftc1a  26014  plyeq0lem  26185  aannenlem3  26308  geolim3  26317  psercnlem1  26405  pserdvlem2  26408  reeff1olem  26426  pilem2  26432  pilem3  26433  cosq14gt0  26488  cosq14ge0  26489  cosne0  26507  recosf1o  26513  resinf1o  26514  argregt0  26588  logcnlem3  26622  logcnlem4  26623  logf1o2  26628  cxpcn3lem  26726  ang180lem2  26789  acosbnd  26879  atanbndlem  26904  leibpi  26921  cxp2lim  26956  emcllem2  26976  ftalem5  27056  basellem9  27068  vmage0  27100  chpge0  27105  chtub  27192  mersenne  27207  bposlem2  27265  bposlem5  27268  bposlem6  27269  bposlem9  27272  gausslemma2dlem0c  27338  gausslemma2dlem0e  27340  lgseisenlem1  27355  lgsquadlem1  27360  lgsquadlem2  27361  lgsquadlem3  27362  chebbnd1lem1  27449  chebbnd1lem2  27450  chebbnd1lem3  27451  mulog2sumlem2  27515  pntpbnd1a  27565  pntibndlem1  27569  pntibndlem3  27572  pntlemc  27575  ostth2  27617  ostth3  27618  absmuls  28204  pthdlem1  29714  numclwlk1lem2  30317  smcnlem  30644  minvecolem2  30822  minvecolem4  30827  strlem5  32202  hstrlem5  32210  abrexdomjm  32454  prct  32661  cyc3conja  33116  elrgspnlem2  33186  prmidl0  33413  fldextrspunlsplem  33660  constrext2chnlem  33730  dya2icoseg  34238  omssubadd  34261  omsmeas  34284  oddpwdc  34315  logdivsqrle  34624  faclim  35705  faclim2  35707  taupilem1  37281  mblfinlem3  37625  mblfinlem4  37626  ibladdnclem  37642  iblmulc2nc  37651  abrexdom  37696  dalem3  39625  dalem8  39631  dalem25  39659  dalem27  39660  dalem38  39671  dalem44  39677  dalem54  39687  lhpat3  40007  4atexlemunv  40027  4atexlemtlw  40028  4atexlemc  40030  4atexlemnclw  40031  4atexlemex2  40032  4atexlemcnd  40033  cdleme0b  40173  cdleme0c  40174  cdleme0fN  40179  cdlemeulpq  40181  cdleme01N  40182  cdleme0ex1N  40184  cdleme2  40189  cdleme3b  40190  cdleme3c  40191  cdleme3g  40195  cdleme3h  40196  cdleme4a  40200  cdleme7aa  40203  cdleme7c  40206  cdleme7d  40207  cdleme7e  40208  cdleme9  40214  cdleme11fN  40225  cdleme11k  40229  cdleme15d  40238  cdlemednpq  40260  cdleme19c  40266  cdleme20aN  40270  cdleme20e  40274  cdleme21c  40288  cdleme21ct  40290  cdleme22e  40305  cdleme22eALTN  40306  cdleme22f  40307  cdleme23a  40310  cdleme28a  40331  cdleme35f  40415  cdlemeg46frv  40486  cdlemeg46rgv  40489  cdlemeg46req  40490  cdlemg2fv2  40561  cdlemg2m  40565  cdlemg6c  40581  cdlemg31a  40658  cdlemg31b  40659  cdlemk10  40804  cdlemk37  40875  dia2dimlem1  41025  dihjatcclem4  41382  imadomfi  41962  aks5lem1  42146  metakunt30  42194  3cubeslem1  42658  irrapxlem3  42798  pell14qrgapw  42850  dgrsub2  43110  radcnvrat  44290  ressiooinf  45527  fmul01  45552  fmul01lt1lem1  45556  fmul01lt1lem2  45557  sumnnodd  45602  climlimsupcex  45741  cnrefiisplem  45801  stoweidlem1  45973  stoweidlem5  45977  stoweidlem7  45979  dirkercncflem1  46075  dirkercncflem4  46078  fourierdlem30  46109  fourierdlem42  46121  fourierdlem48  46126  fourierdlem62  46140  fourierdlem63  46141  fourierdlem68  46146  fourierdlem79  46157  sqwvfoura  46200  etransclem32  46238  hoidmvlelem2  46568  iunhoiioolem  46647  vonioolem1  46652  pimdecfgtioo  46689  pimincfltioo  46690  smfmullem1  46763  m1modnep2mod  47312  fmtnoge3  47475  fmtnoprmfac2lem1  47511  sfprmdvdsmersenne  47548  lighneallem2  47551  lighneallem4a  47553  proththdlem  47558  stgoldbwt  47721  sgoldbeven3prm  47728  mogoldbb  47730  evengpop3  47743  bgoldbtbndlem2  47751  bgoldbtbndlem3  47752  2ltceilhalf  47973  lindslinindimp2lem3  48335  fllogbd  48439  nnolog2flm1  48469