Theorem eqbrtrid 5065

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  map1  8575  xp1en  8586  map2xp  8671  1sdom  8705  sucxpdom  8711  sniffsupp  8857  wdomima2g  9034  endjudisj  9579  dju1dif  9583  mapdjuen  9591  djuxpdom  9596  djufi  9597  pwsdompw  9615  infunsdom1  9624  infunsdom  9625  infxp  9626  ackbij1lem5  9635  hsmexlem4  9840  imadomg  9945  unidom  9954  unictb  9986  pwxpndom2  10076  pwdjundom  10078  distrnq  10372  nnne0  11659  supxrmnf  12698  xov1plusxeqvd  12876  quoremz  13218  quoremnn0ALT  13220  intfrac2  13221  m1modge3gt1  13281  bernneq2  13587  faclbnd4lem1  13649  sqrlem4  14597  reccn2  14945  caucvg  15027  o1fsum  15160  infcvgaux2i  15205  eirrlem  15549  rpnnen2lem12  15570  ruclem12  15586  nno  15723  divalglem5  15738  bitsfzolem  15773  bitsinv1lem  15780  bezoutlem3  15879  lcmfunsnlem  15975  coprmproddvds  15997  oddprmge3  16034  ge2nprmge4  16035  sqnprm  16036  prmreclem6  16247  4sqlem6  16269  4sqlem13  16283  4sqlem16  16286  4sqlem17  16287  2expltfac  16418  odcau  18721  sylow3  18750  efginvrel2  18845  lt6abl  19008  ablfac1lem  19183  gzrngunitlem  20156  zringlpirlem3  20179  znfld  20252  evlslem2  20751  chfacffsupp  21461  cpmidpmatlem3  21477  cctop  21611  csdfil  22499  xpsdsval  22988  nrginvrcnlem  23297  icccmplem2  23428  reconnlem2  23432  iscmet3lem3  23894  minveclem2  24030  minveclem4  24036  ivthlem2  24056  ivthlem3  24057  ovolunlem1a  24100  ovolfiniun  24105  ovoliunlem3  24108  ovoliun  24109  ovolicc2lem4  24124  unmbl  24141  ioombl1lem4  24165  itg2mono  24357  ibladdlem  24423  iblabsr  24433  iblmulc2  24434  bddiblnc  24445  dvferm1lem  24587  dvferm2lem  24589  lhop1lem  24616  dvcvx  24623  ftc1a  24640  plyeq0lem  24807  aannenlem3  24926  geolim3  24935  psercnlem1  25020  pserdvlem2  25023  reeff1olem  25041  pilem2  25047  pilem3  25048  cosq14gt0  25103  cosq14ge0  25104  cosne0  25121  recosf1o  25127  resinf1o  25128  argregt0  25201  logcnlem3  25235  logcnlem4  25236  logf1o2  25241  cxpcn3lem  25336  ang180lem2  25396  acosbnd  25486  atanbndlem  25511  leibpi  25528  cxp2lim  25562  emcllem2  25582  ftalem5  25662  basellem9  25674  vmage0  25706  chpge0  25711  chtub  25796  mersenne  25811  bposlem2  25869  bposlem5  25872  bposlem6  25873  bposlem9  25876  gausslemma2dlem0c  25942  gausslemma2dlem0e  25944  lgseisenlem1  25959  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  mulog2sumlem2  26119  pntpbnd1a  26169  pntibndlem1  26173  pntibndlem3  26176  pntlemc  26179  ostth2  26221  ostth3  26222  pthdlem1  27555  numclwlk1lem2  28155  smcnlem  28480  minvecolem2  28658  minvecolem4  28663  strlem5  30038  hstrlem5  30046  abrexdomjm  30275  prct  30476  cyc3conja  30849  dvdschrmulg  30908  prmidl0  31034  dya2icoseg  31645  omssubadd  31668  omsmeas  31691  oddpwdc  31722  logdivsqrle  32031  faclim  33091  faclim2  33093  taupilem1  34735  mblfinlem3  35096  mblfinlem4  35097  ibladdnclem  35113  iblmulc2nc  35122  abrexdom  35168  dalem3  36960  dalem8  36966  dalem25  36994  dalem27  36995  dalem38  37006  dalem44  37012  dalem54  37022  lhpat3  37342  4atexlemunv  37362  4atexlemtlw  37363  4atexlemc  37365  4atexlemnclw  37366  4atexlemex2  37367  4atexlemcnd  37368  cdleme0b  37508  cdleme0c  37509  cdleme0fN  37514  cdlemeulpq  37516  cdleme01N  37517  cdleme0ex1N  37519  cdleme2  37524  cdleme3b  37525  cdleme3c  37526  cdleme3g  37530  cdleme3h  37531  cdleme4a  37535  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme9  37549  cdleme11fN  37560  cdleme11k  37564  cdleme15d  37573  cdlemednpq  37595  cdleme19c  37601  cdleme20aN  37605  cdleme20e  37609  cdleme21c  37623  cdleme21ct  37625  cdleme22e  37640  cdleme22eALTN  37641  cdleme22f  37642  cdleme23a  37645  cdleme28a  37666  cdleme35f  37750  cdlemeg46frv  37821  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemg2fv2  37896  cdlemg2m  37900  cdlemg6c  37916  cdlemg31a  37993  cdlemg31b  37994  cdlemk10  38139  cdlemk37  38210  dia2dimlem1  38360  dihjatcclem4  38717  metakunt30  39379  3cubeslem1  39625  irrapxlem3  39765  pell14qrgapw  39817  dgrsub2  40079  radcnvrat  41018  ressiooinf  42194  fmul01  42222  fmul01lt1lem1  42226  fmul01lt1lem2  42227  sumnnodd  42272  climlimsupcex  42411  cnrefiisplem  42471  stoweidlem1  42643  stoweidlem5  42647  stoweidlem7  42649  dirkercncflem1  42745  dirkercncflem4  42748  fourierdlem30  42779  fourierdlem42  42791  fourierdlem48  42796  fourierdlem62  42810  fourierdlem63  42811  fourierdlem68  42816  fourierdlem79  42827  sqwvfoura  42870  etransclem32  42908  hoidmvlelem2  43235  iunhoiioolem  43314  vonioolem1  43319  pimdecfgtioo  43352  pimincfltioo  43353  smfmullem1  43423  fmtnoge3  44047  fmtnoprmfac2lem1  44083  sfprmdvdsmersenne  44121  lighneallem2  44124  lighneallem4a  44126  proththdlem  44131  stgoldbwt  44294  sgoldbeven3prm  44301  mogoldbb  44303  evengpop3  44316  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  lindslinindimp2lem3  44869  fllogbd  44974  nnolog2flm1  45004