Theorem eqbrtrid 5105

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  map1  8784  xp1en  8798  map2xp  8883  1sdom  8955  sucxpdom  8961  sniffsupp  9089  wdomima2g  9275  endjudisj  9855  dju1dif  9859  mapdjuen  9867  djuxpdom  9872  djufi  9873  pwsdompw  9891  infunsdom1  9900  infunsdom  9901  infxp  9902  ackbij1lem5  9911  hsmexlem4  10116  imadomg  10221  unidom  10230  unictb  10262  pwxpndom2  10352  pwdjundom  10354  distrnq  10648  nnne0  11937  supxrmnf  12980  xov1plusxeqvd  13159  quoremz  13503  quoremnn0ALT  13505  intfrac2  13506  m1modge3gt1  13566  bernneq2  13873  faclbnd4lem1  13935  sqrlem4  14885  reccn2  15234  caucvg  15318  o1fsum  15453  infcvgaux2i  15498  eirrlem  15841  rpnnen2lem12  15862  ruclem12  15878  nno  16019  divalglem5  16034  bitsfzolem  16069  bitsinv1lem  16076  bezoutlem3  16177  lcmfunsnlem  16274  coprmproddvds  16296  oddprmge3  16333  ge2nprmge4  16334  sqnprm  16335  prmreclem6  16550  4sqlem6  16572  4sqlem13  16586  4sqlem16  16589  4sqlem17  16590  2expltfac  16722  odcau  19124  sylow3  19153  efginvrel2  19248  lt6abl  19411  ablfac1lem  19586  gzrngunitlem  20575  zringlpirlem3  20598  znfld  20680  evlslem2  21199  chfacffsupp  21913  cpmidpmatlem3  21929  cctop  22064  csdfil  22953  xpsdsval  23442  nrginvrcnlem  23761  icccmplem2  23892  reconnlem2  23896  iscmet3lem3  24359  minveclem2  24495  minveclem4  24501  ivthlem2  24521  ivthlem3  24522  ovolunlem1a  24565  ovolfiniun  24570  ovoliunlem3  24573  ovoliun  24574  ovolicc2lem4  24589  unmbl  24606  ioombl1lem4  24630  itg2mono  24823  ibladdlem  24889  iblabsr  24899  iblmulc2  24900  bddiblnc  24911  dvferm1lem  25053  dvferm2lem  25055  lhop1lem  25082  dvcvx  25089  ftc1a  25106  plyeq0lem  25276  aannenlem3  25395  geolim3  25404  psercnlem1  25489  pserdvlem2  25492  reeff1olem  25510  pilem2  25516  pilem3  25517  cosq14gt0  25572  cosq14ge0  25573  cosne0  25590  recosf1o  25596  resinf1o  25597  argregt0  25670  logcnlem3  25704  logcnlem4  25705  logf1o2  25710  cxpcn3lem  25805  ang180lem2  25865  acosbnd  25955  atanbndlem  25980  leibpi  25997  cxp2lim  26031  emcllem2  26051  ftalem5  26131  basellem9  26143  vmage0  26175  chpge0  26180  chtub  26265  mersenne  26280  bposlem2  26338  bposlem5  26341  bposlem6  26342  bposlem9  26345  gausslemma2dlem0c  26411  gausslemma2dlem0e  26413  lgseisenlem1  26428  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  mulog2sumlem2  26588  pntpbnd1a  26638  pntibndlem1  26642  pntibndlem3  26645  pntlemc  26648  ostth2  26690  ostth3  26691  pthdlem1  28035  numclwlk1lem2  28635  smcnlem  28960  minvecolem2  29138  minvecolem4  29143  strlem5  30518  hstrlem5  30526  abrexdomjm  30753  prct  30951  cyc3conja  31326  dvdschrmulg  31385  prmidl0  31528  dya2icoseg  32144  omssubadd  32167  omsmeas  32190  oddpwdc  32221  logdivsqrle  32530  faclim  33618  faclim2  33620  taupilem1  35419  mblfinlem3  35743  mblfinlem4  35744  ibladdnclem  35760  iblmulc2nc  35769  abrexdom  35815  dalem3  37605  dalem8  37611  dalem25  37639  dalem27  37640  dalem38  37651  dalem44  37657  dalem54  37667  lhpat3  37987  4atexlemunv  38007  4atexlemtlw  38008  4atexlemc  38010  4atexlemnclw  38011  4atexlemex2  38012  4atexlemcnd  38013  cdleme0b  38153  cdleme0c  38154  cdleme0fN  38159  cdlemeulpq  38161  cdleme01N  38162  cdleme0ex1N  38164  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme3g  38175  cdleme3h  38176  cdleme4a  38180  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme9  38194  cdleme11fN  38205  cdleme11k  38209  cdleme15d  38218  cdlemednpq  38240  cdleme19c  38246  cdleme20aN  38250  cdleme20e  38254  cdleme21c  38268  cdleme21ct  38270  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme23a  38290  cdleme28a  38311  cdleme35f  38395  cdlemeg46frv  38466  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg6c  38561  cdlemg31a  38638  cdlemg31b  38639  cdlemk10  38784  cdlemk37  38855  dia2dimlem1  39005  dihjatcclem4  39362  metakunt30  40082  3cubeslem1  40422  irrapxlem3  40562  pell14qrgapw  40614  dgrsub2  40876  radcnvrat  41821  ressiooinf  42985  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  sumnnodd  43061  climlimsupcex  43200  cnrefiisplem  43260  stoweidlem1  43432  stoweidlem5  43436  stoweidlem7  43438  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem30  43568  fourierdlem42  43580  fourierdlem48  43585  fourierdlem62  43599  fourierdlem63  43600  fourierdlem68  43605  fourierdlem79  43616  sqwvfoura  43659  etransclem32  43697  hoidmvlelem2  44024  iunhoiioolem  44103  vonioolem1  44108  pimdecfgtioo  44141  pimincfltioo  44142  smfmullem1  44212  fmtnoge3  44870  fmtnoprmfac2lem1  44906  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem4a  44948  proththdlem  44953  stgoldbwt  45116  sgoldbeven3prm  45123  mogoldbb  45125  evengpop3  45138  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  lindslinindimp2lem3  45689  fllogbd  45794  nnolog2flm1  45824