Theorem eqbrtrid 5201

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  map1  9105  xp1en  9123  map2xp  9213  rex2dom  9309  1sdomOLD  9312  sucxpdom  9318  sniffsupp  9469  wdomima2g  9655  endjudisj  10238  dju1dif  10242  mapdjuen  10250  djuxpdom  10255  djufi  10256  pwsdompw  10272  infunsdom1  10281  infunsdom  10282  infxp  10283  ackbij1lem5  10292  hsmexlem4  10498  imadomg  10603  unidom  10612  unictb  10644  pwxpndom2  10734  pwdjundom  10736  distrnq  11030  nnne0  12327  supxrmnf  13379  xov1plusxeqvd  13558  quoremz  13906  quoremnn0ALT  13908  intfrac2  13909  m1modge3gt1  13969  bernneq2  14279  faclbnd4lem1  14342  01sqrexlem4  15294  reccn2  15643  caucvg  15727  o1fsum  15861  infcvgaux2i  15906  eirrlem  16252  rpnnen2lem12  16273  ruclem12  16289  nno  16430  divalglem5  16445  bitsfzolem  16480  bitsinv1lem  16487  bezoutlem3  16588  lcmfunsnlem  16688  coprmproddvds  16710  oddprmge3  16747  ge2nprmge4  16748  sqnprm  16749  prmreclem6  16968  4sqlem6  16990  4sqlem13  17004  4sqlem16  17007  4sqlem17  17008  2expltfac  17140  odcau  19646  sylow3  19675  efginvrel2  19769  lt6abl  19937  ablfac1lem  20112  gzrngunitlem  21473  zringlpirlem3  21498  dvdschrmulg  21566  znfld  21602  evlslem2  22126  chfacffsupp  22883  cpmidpmatlem3  22899  cctop  23034  csdfil  23923  xpsdsval  24412  nrginvrcnlem  24733  icccmplem2  24864  reconnlem2  24868  iscmet3lem3  25343  minveclem2  25479  minveclem4  25485  ivthlem2  25506  ivthlem3  25507  ovolunlem1a  25550  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovolicc2lem4  25574  unmbl  25591  ioombl1lem4  25615  itg2mono  25808  ibladdlem  25875  iblabsr  25885  iblmulc2  25886  bddiblnc  25897  dvferm1lem  26042  dvferm2lem  26044  lhop1lem  26072  dvcvx  26079  ftc1a  26098  plyeq0lem  26269  aannenlem3  26390  geolim3  26399  psercnlem1  26487  pserdvlem2  26490  reeff1olem  26508  pilem2  26514  pilem3  26515  cosq14gt0  26570  cosq14ge0  26571  cosne0  26589  recosf1o  26595  resinf1o  26596  argregt0  26670  logcnlem3  26704  logcnlem4  26705  logf1o2  26710  cxpcn3lem  26808  ang180lem2  26871  acosbnd  26961  atanbndlem  26986  leibpi  27003  cxp2lim  27038  emcllem2  27058  ftalem5  27138  basellem9  27150  vmage0  27182  chpge0  27187  chtub  27274  mersenne  27289  bposlem2  27347  bposlem5  27350  bposlem6  27351  bposlem9  27354  gausslemma2dlem0c  27420  gausslemma2dlem0e  27422  lgseisenlem1  27437  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  mulog2sumlem2  27597  pntpbnd1a  27647  pntibndlem1  27651  pntibndlem3  27654  pntlemc  27657  ostth2  27699  ostth3  27700  absmuls  28286  pthdlem1  29802  numclwlk1lem2  30402  smcnlem  30729  minvecolem2  30907  minvecolem4  30912  strlem5  32287  hstrlem5  32295  abrexdomjm  32535  prct  32728  cyc3conja  33150  prmidl0  33443  dya2icoseg  34242  omssubadd  34265  omsmeas  34288  oddpwdc  34319  logdivsqrle  34627  faclim  35708  faclim2  35710  taupilem1  37287  mblfinlem3  37619  mblfinlem4  37620  ibladdnclem  37636  iblmulc2nc  37645  abrexdom  37690  dalem3  39621  dalem8  39627  dalem25  39655  dalem27  39656  dalem38  39667  dalem44  39673  dalem54  39683  lhpat3  40003  4atexlemunv  40023  4atexlemtlw  40024  4atexlemc  40026  4atexlemnclw  40027  4atexlemex2  40028  4atexlemcnd  40029  cdleme0b  40169  cdleme0c  40170  cdleme0fN  40175  cdlemeulpq  40177  cdleme01N  40178  cdleme0ex1N  40180  cdleme2  40185  cdleme3b  40186  cdleme3c  40187  cdleme3g  40191  cdleme3h  40192  cdleme4a  40196  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme9  40210  cdleme11fN  40221  cdleme11k  40225  cdleme15d  40234  cdlemednpq  40256  cdleme19c  40262  cdleme20aN  40266  cdleme20e  40270  cdleme21c  40284  cdleme21ct  40286  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme23a  40306  cdleme28a  40327  cdleme35f  40411  cdlemeg46frv  40482  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemg2fv2  40557  cdlemg2m  40561  cdlemg6c  40577  cdlemg31a  40654  cdlemg31b  40655  cdlemk10  40800  cdlemk37  40871  dia2dimlem1  41021  dihjatcclem4  41378  imadomfi  41959  aks5lem1  42143  metakunt30  42191  3cubeslem1  42640  irrapxlem3  42780  pell14qrgapw  42832  dgrsub2  43092  radcnvrat  44283  ressiooinf  45475  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1lem2  45506  sumnnodd  45551  climlimsupcex  45690  cnrefiisplem  45750  stoweidlem1  45922  stoweidlem5  45926  stoweidlem7  45928  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem30  46058  fourierdlem42  46070  fourierdlem48  46075  fourierdlem62  46089  fourierdlem63  46090  fourierdlem68  46095  fourierdlem79  46106  sqwvfoura  46149  etransclem32  46187  hoidmvlelem2  46517  iunhoiioolem  46596  vonioolem1  46601  pimdecfgtioo  46638  pimincfltioo  46639  smfmullem1  46712  fmtnoge3  47404  fmtnoprmfac2lem1  47440  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem4a  47482  proththdlem  47487  stgoldbwt  47650  sgoldbeven3prm  47657  mogoldbb  47659  evengpop3  47672  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  lindslinindimp2lem3  48189  fllogbd  48294  nnolog2flm1  48324