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

Syntax hints:   → wi 4   = wceq 1539   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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  map1  9042  xp1en  9059  map2xp  9149  rex2dom  9248  1sdomOLD  9251  sucxpdom  9257  sniffsupp  9397  wdomima2g  9583  endjudisj  10165  dju1dif  10169  mapdjuen  10177  djuxpdom  10182  djufi  10183  pwsdompw  10201  infunsdom1  10210  infunsdom  10211  infxp  10212  ackbij1lem5  10221  hsmexlem4  10426  imadomg  10531  unidom  10540  unictb  10572  pwxpndom2  10662  pwdjundom  10664  distrnq  10958  nnne0  12250  supxrmnf  13300  xov1plusxeqvd  13479  quoremz  13824  quoremnn0ALT  13826  intfrac2  13827  m1modge3gt1  13887  bernneq2  14197  faclbnd4lem1  14257  01sqrexlem4  15196  reccn2  15545  caucvg  15629  o1fsum  15763  infcvgaux2i  15808  eirrlem  16151  rpnnen2lem12  16172  ruclem12  16188  nno  16329  divalglem5  16344  bitsfzolem  16379  bitsinv1lem  16386  bezoutlem3  16487  lcmfunsnlem  16582  coprmproddvds  16604  oddprmge3  16641  ge2nprmge4  16642  sqnprm  16643  prmreclem6  16858  4sqlem6  16880  4sqlem13  16894  4sqlem16  16897  4sqlem17  16898  2expltfac  17030  odcau  19513  sylow3  19542  efginvrel2  19636  lt6abl  19804  ablfac1lem  19979  gzrngunitlem  21210  zringlpirlem3  21235  znfld  21335  evlslem2  21861  chfacffsupp  22578  cpmidpmatlem3  22594  cctop  22729  csdfil  23618  xpsdsval  24107  nrginvrcnlem  24428  icccmplem2  24559  reconnlem2  24563  iscmet3lem3  25038  minveclem2  25174  minveclem4  25180  ivthlem2  25201  ivthlem3  25202  ovolunlem1a  25245  ovolfiniun  25250  ovoliunlem3  25253  ovoliun  25254  ovolicc2lem4  25269  unmbl  25286  ioombl1lem4  25310  itg2mono  25503  ibladdlem  25569  iblabsr  25579  iblmulc2  25580  bddiblnc  25591  dvferm1lem  25736  dvferm2lem  25738  lhop1lem  25765  dvcvx  25772  ftc1a  25789  plyeq0lem  25959  aannenlem3  26079  geolim3  26088  psercnlem1  26173  pserdvlem2  26176  reeff1olem  26194  pilem2  26200  pilem3  26201  cosq14gt0  26256  cosq14ge0  26257  cosne0  26274  recosf1o  26280  resinf1o  26281  argregt0  26354  logcnlem3  26388  logcnlem4  26389  logf1o2  26394  cxpcn3lem  26491  ang180lem2  26551  acosbnd  26641  atanbndlem  26666  leibpi  26683  cxp2lim  26717  emcllem2  26737  ftalem5  26817  basellem9  26829  vmage0  26861  chpge0  26866  chtub  26951  mersenne  26966  bposlem2  27024  bposlem5  27027  bposlem6  27028  bposlem9  27031  gausslemma2dlem0c  27097  gausslemma2dlem0e  27099  lgseisenlem1  27114  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  chebbnd1lem1  27208  chebbnd1lem2  27209  chebbnd1lem3  27210  mulog2sumlem2  27274  pntpbnd1a  27324  pntibndlem1  27328  pntibndlem3  27331  pntlemc  27334  ostth2  27376  ostth3  27377  pthdlem1  29290  numclwlk1lem2  29890  smcnlem  30217  minvecolem2  30395  minvecolem4  30400  strlem5  31775  hstrlem5  31783  abrexdomjm  32011  prct  32206  cyc3conja  32586  dvdschrmulg  32650  prmidl0  32843  dya2icoseg  33574  omssubadd  33597  omsmeas  33620  oddpwdc  33651  logdivsqrle  33960  faclim  35020  faclim2  35022  taupilem1  36505  mblfinlem3  36830  mblfinlem4  36831  ibladdnclem  36847  iblmulc2nc  36856  abrexdom  36901  dalem3  38838  dalem8  38844  dalem25  38872  dalem27  38873  dalem38  38884  dalem44  38890  dalem54  38900  lhpat3  39220  4atexlemunv  39240  4atexlemtlw  39241  4atexlemc  39243  4atexlemnclw  39244  4atexlemex2  39245  4atexlemcnd  39246  cdleme0b  39386  cdleme0c  39387  cdleme0fN  39392  cdlemeulpq  39394  cdleme01N  39395  cdleme0ex1N  39397  cdleme2  39402  cdleme3b  39403  cdleme3c  39404  cdleme3g  39408  cdleme3h  39409  cdleme4a  39413  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme9  39427  cdleme11fN  39438  cdleme11k  39442  cdleme15d  39451  cdlemednpq  39473  cdleme19c  39479  cdleme20aN  39483  cdleme20e  39487  cdleme21c  39501  cdleme21ct  39503  cdleme22e  39518  cdleme22eALTN  39519  cdleme22f  39520  cdleme23a  39523  cdleme28a  39544  cdleme35f  39628  cdlemeg46frv  39699  cdlemeg46rgv  39702  cdlemeg46req  39703  cdlemg2fv2  39774  cdlemg2m  39778  cdlemg6c  39794  cdlemg31a  39871  cdlemg31b  39872  cdlemk10  40017  cdlemk37  40088  dia2dimlem1  40238  dihjatcclem4  40595  metakunt30  41320  3cubeslem1  41724  irrapxlem3  41864  pell14qrgapw  41916  dgrsub2  42179  radcnvrat  43375  ressiooinf  44568  fmul01  44594  fmul01lt1lem1  44598  fmul01lt1lem2  44599  sumnnodd  44644  climlimsupcex  44783  cnrefiisplem  44843  stoweidlem1  45015  stoweidlem5  45019  stoweidlem7  45021  dirkercncflem1  45117  dirkercncflem4  45120  fourierdlem30  45151  fourierdlem42  45163  fourierdlem48  45168  fourierdlem62  45182  fourierdlem63  45183  fourierdlem68  45188  fourierdlem79  45199  sqwvfoura  45242  etransclem32  45280  hoidmvlelem2  45610  iunhoiioolem  45689  vonioolem1  45694  pimdecfgtioo  45731  pimincfltioo  45732  smfmullem1  45805  fmtnoge3  46496  fmtnoprmfac2lem1  46532  sfprmdvdsmersenne  46569  lighneallem2  46572  lighneallem4a  46574  proththdlem  46579  stgoldbwt  46742  sgoldbeven3prm  46749  mogoldbb  46751  evengpop3  46764  bgoldbtbndlem2  46772  bgoldbtbndlem3  46773  lindslinindimp2lem3  47228  fllogbd  47333  nnolog2flm1  47363