Theorem eqbrtrid 5182

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  map1  9078  xp1en  9095  map2xp  9185  rex2dom  9279  1sdomOLD  9282  sucxpdom  9288  sniffsupp  9437  wdomima2g  9623  endjudisj  10206  dju1dif  10210  mapdjuen  10218  djuxpdom  10223  djufi  10224  pwsdompw  10240  infunsdom1  10249  infunsdom  10250  infxp  10251  ackbij1lem5  10260  hsmexlem4  10466  imadomg  10571  unidom  10580  unictb  10612  pwxpndom2  10702  pwdjundom  10704  distrnq  10998  nnne0  12297  supxrmnf  13355  xov1plusxeqvd  13534  quoremz  13891  quoremnn0ALT  13893  intfrac2  13894  m1modge3gt1  13955  bernneq2  14265  faclbnd4lem1  14328  01sqrexlem4  15280  reccn2  15629  caucvg  15711  o1fsum  15845  infcvgaux2i  15890  eirrlem  16236  rpnnen2lem12  16257  ruclem12  16273  nno  16415  divalglem5  16430  bitsfzolem  16467  bitsinv1lem  16474  bezoutlem3  16574  lcmfunsnlem  16674  coprmproddvds  16696  oddprmge3  16733  ge2nprmge4  16734  sqnprm  16735  prmreclem6  16954  4sqlem6  16976  4sqlem13  16990  4sqlem16  16993  4sqlem17  16994  2expltfac  17126  odcau  19636  sylow3  19665  efginvrel2  19759  lt6abl  19927  ablfac1lem  20102  gzrngunitlem  21467  zringlpirlem3  21492  dvdschrmulg  21560  znfld  21596  evlslem2  22120  chfacffsupp  22877  cpmidpmatlem3  22893  cctop  23028  csdfil  23917  xpsdsval  24406  nrginvrcnlem  24727  icccmplem2  24858  reconnlem2  24862  iscmet3lem3  25337  minveclem2  25473  minveclem4  25479  ivthlem2  25500  ivthlem3  25501  ovolunlem1a  25544  ovolfiniun  25549  ovoliunlem3  25552  ovoliun  25553  ovolicc2lem4  25568  unmbl  25585  ioombl1lem4  25609  itg2mono  25802  ibladdlem  25869  iblabsr  25879  iblmulc2  25880  bddiblnc  25891  dvferm1lem  26036  dvferm2lem  26038  lhop1lem  26066  dvcvx  26073  ftc1a  26092  plyeq0lem  26263  aannenlem3  26386  geolim3  26395  psercnlem1  26483  pserdvlem2  26486  reeff1olem  26504  pilem2  26510  pilem3  26511  cosq14gt0  26566  cosq14ge0  26567  cosne0  26585  recosf1o  26591  resinf1o  26592  argregt0  26666  logcnlem3  26700  logcnlem4  26701  logf1o2  26706  cxpcn3lem  26804  ang180lem2  26867  acosbnd  26957  atanbndlem  26982  leibpi  26999  cxp2lim  27034  emcllem2  27054  ftalem5  27134  basellem9  27146  vmage0  27178  chpge0  27183  chtub  27270  mersenne  27285  bposlem2  27343  bposlem5  27346  bposlem6  27347  bposlem9  27350  gausslemma2dlem0c  27416  gausslemma2dlem0e  27418  lgseisenlem1  27433  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  chebbnd1lem1  27527  chebbnd1lem2  27528  chebbnd1lem3  27529  mulog2sumlem2  27593  pntpbnd1a  27643  pntibndlem1  27647  pntibndlem3  27650  pntlemc  27653  ostth2  27695  ostth3  27696  absmuls  28282  pthdlem1  29798  numclwlk1lem2  30398  smcnlem  30725  minvecolem2  30903  minvecolem4  30908  strlem5  32283  hstrlem5  32291  abrexdomjm  32534  prct  32731  cyc3conja  33159  elrgspnlem2  33232  prmidl0  33457  dya2icoseg  34258  omssubadd  34281  omsmeas  34304  oddpwdc  34335  logdivsqrle  34643  faclim  35725  faclim2  35727  taupilem1  37303  mblfinlem3  37645  mblfinlem4  37646  ibladdnclem  37662  iblmulc2nc  37671  abrexdom  37716  dalem3  39646  dalem8  39652  dalem25  39680  dalem27  39681  dalem38  39692  dalem44  39698  dalem54  39708  lhpat3  40028  4atexlemunv  40048  4atexlemtlw  40049  4atexlemc  40051  4atexlemnclw  40052  4atexlemex2  40053  4atexlemcnd  40054  cdleme0b  40194  cdleme0c  40195  cdleme0fN  40200  cdlemeulpq  40202  cdleme01N  40203  cdleme0ex1N  40205  cdleme2  40210  cdleme3b  40211  cdleme3c  40212  cdleme3g  40216  cdleme3h  40217  cdleme4a  40221  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme9  40235  cdleme11fN  40246  cdleme11k  40250  cdleme15d  40259  cdlemednpq  40281  cdleme19c  40287  cdleme20aN  40291  cdleme20e  40295  cdleme21c  40309  cdleme21ct  40311  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme23a  40331  cdleme28a  40352  cdleme35f  40436  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg6c  40602  cdlemg31a  40679  cdlemg31b  40680  cdlemk10  40825  cdlemk37  40896  dia2dimlem1  41046  dihjatcclem4  41403  imadomfi  41983  aks5lem1  42167  metakunt30  42215  3cubeslem1  42671  irrapxlem3  42811  pell14qrgapw  42863  dgrsub2  43123  radcnvrat  44309  ressiooinf  45509  fmul01  45535  fmul01lt1lem1  45539  fmul01lt1lem2  45540  sumnnodd  45585  climlimsupcex  45724  cnrefiisplem  45784  stoweidlem1  45956  stoweidlem5  45960  stoweidlem7  45962  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem30  46092  fourierdlem42  46104  fourierdlem48  46109  fourierdlem62  46123  fourierdlem63  46124  fourierdlem68  46129  fourierdlem79  46140  sqwvfoura  46183  etransclem32  46221  hoidmvlelem2  46551  iunhoiioolem  46630  vonioolem1  46635  pimdecfgtioo  46672  pimincfltioo  46673  smfmullem1  46746  m1modnep2mod  47291  fmtnoge3  47454  fmtnoprmfac2lem1  47490  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem4a  47532  proththdlem  47537  stgoldbwt  47700  sgoldbeven3prm  47707  mogoldbb  47709  evengpop3  47722  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  2ltceilhalf  47949  lindslinindimp2lem3  48305  fllogbd  48409  nnolog2flm1  48439