Theorem eqbrtrid 5159

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5124

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  map1  9059  xp1en  9076  map2xp  9166  rex2dom  9259  1sdomOLD  9262  sucxpdom  9268  sniffsupp  9417  wdomima2g  9605  endjudisj  10188  dju1dif  10192  mapdjuen  10200  djuxpdom  10205  djufi  10206  pwsdompw  10222  infunsdom1  10231  infunsdom  10232  infxp  10233  ackbij1lem5  10242  hsmexlem4  10448  imadomg  10553  unidom  10562  unictb  10594  pwxpndom2  10684  pwdjundom  10686  distrnq  10980  nnne0  12279  supxrmnf  13338  xov1plusxeqvd  13520  quoremz  13877  quoremnn0ALT  13879  intfrac2  13880  m1modge3gt1  13941  bernneq2  14253  faclbnd4lem1  14316  01sqrexlem4  15269  reccn2  15618  caucvg  15700  o1fsum  15834  infcvgaux2i  15879  eirrlem  16227  rpnnen2lem12  16248  ruclem12  16264  nno  16406  divalglem5  16421  bitsfzolem  16458  bitsinv1lem  16465  bezoutlem3  16565  lcmfunsnlem  16665  coprmproddvds  16687  oddprmge3  16724  ge2nprmge4  16725  sqnprm  16726  prmreclem6  16946  4sqlem6  16968  4sqlem13  16982  4sqlem16  16985  4sqlem17  16986  2expltfac  17117  odcau  19590  sylow3  19619  efginvrel2  19713  lt6abl  19881  ablfac1lem  20056  gzrngunitlem  21405  zringlpirlem3  21430  dvdschrmulg  21494  znfld  21526  evlslem2  22042  chfacffsupp  22799  cpmidpmatlem3  22815  cctop  22949  csdfil  23837  xpsdsval  24325  nrginvrcnlem  24635  icccmplem2  24768  reconnlem2  24772  iscmet3lem3  25247  minveclem2  25383  minveclem4  25389  ivthlem2  25410  ivthlem3  25411  ovolunlem1a  25454  ovolfiniun  25459  ovoliunlem3  25462  ovoliun  25463  ovolicc2lem4  25478  unmbl  25495  ioombl1lem4  25519  itg2mono  25711  ibladdlem  25778  iblabsr  25788  iblmulc2  25789  bddiblnc  25800  dvferm1lem  25945  dvferm2lem  25947  lhop1lem  25975  dvcvx  25982  ftc1a  26001  plyeq0lem  26172  aannenlem3  26295  geolim3  26304  psercnlem1  26392  pserdvlem2  26395  reeff1olem  26413  pilem2  26419  pilem3  26420  cosq14gt0  26476  cosq14ge0  26477  cosne0  26495  recosf1o  26501  resinf1o  26502  argregt0  26576  logcnlem3  26610  logcnlem4  26611  logf1o2  26616  cxpcn3lem  26714  ang180lem2  26777  acosbnd  26867  atanbndlem  26892  leibpi  26909  cxp2lim  26944  emcllem2  26964  ftalem5  27044  basellem9  27056  vmage0  27088  chpge0  27093  chtub  27180  mersenne  27195  bposlem2  27253  bposlem5  27256  bposlem6  27257  bposlem9  27260  gausslemma2dlem0c  27326  gausslemma2dlem0e  27328  lgseisenlem1  27343  lgsquadlem1  27348  lgsquadlem2  27349  lgsquadlem3  27350  chebbnd1lem1  27437  chebbnd1lem2  27438  chebbnd1lem3  27439  mulog2sumlem2  27503  pntpbnd1a  27553  pntibndlem1  27557  pntibndlem3  27560  pntlemc  27563  ostth2  27605  ostth3  27606  absmuls  28203  pthdlem1  29753  numclwlk1lem2  30356  smcnlem  30683  minvecolem2  30861  minvecolem4  30866  strlem5  32241  hstrlem5  32249  abrexdomjm  32493  prct  32697  cyc3conja  33173  elrgspnlem2  33243  prmidl0  33470  fldextrspunlsplem  33719  constrext2chnlem  33789  dya2icoseg  34314  omssubadd  34337  omsmeas  34360  oddpwdc  34391  logdivsqrle  34687  faclim  35768  faclim2  35770  taupilem1  37344  mblfinlem3  37688  mblfinlem4  37689  ibladdnclem  37705  iblmulc2nc  37714  abrexdom  37759  dalem3  39688  dalem8  39694  dalem25  39722  dalem27  39723  dalem38  39734  dalem44  39740  dalem54  39750  lhpat3  40070  4atexlemunv  40090  4atexlemtlw  40091  4atexlemc  40093  4atexlemnclw  40094  4atexlemex2  40095  4atexlemcnd  40096  cdleme0b  40236  cdleme0c  40237  cdleme0fN  40242  cdlemeulpq  40244  cdleme01N  40245  cdleme0ex1N  40247  cdleme2  40252  cdleme3b  40253  cdleme3c  40254  cdleme3g  40258  cdleme3h  40259  cdleme4a  40263  cdleme7aa  40266  cdleme7c  40269  cdleme7d  40270  cdleme7e  40271  cdleme9  40277  cdleme11fN  40288  cdleme11k  40292  cdleme15d  40301  cdlemednpq  40323  cdleme19c  40329  cdleme20aN  40333  cdleme20e  40337  cdleme21c  40351  cdleme21ct  40353  cdleme22e  40368  cdleme22eALTN  40369  cdleme22f  40370  cdleme23a  40373  cdleme28a  40394  cdleme35f  40478  cdlemeg46frv  40549  cdlemeg46rgv  40552  cdlemeg46req  40553  cdlemg2fv2  40624  cdlemg2m  40628  cdlemg6c  40644  cdlemg31a  40721  cdlemg31b  40722  cdlemk10  40867  cdlemk37  40938  dia2dimlem1  41088  dihjatcclem4  41445  imadomfi  42020  aks5lem1  42204  3cubeslem1  42682  irrapxlem3  42822  pell14qrgapw  42874  dgrsub2  43134  radcnvrat  44313  ressiooinf  45566  fmul01  45589  fmul01lt1lem1  45593  fmul01lt1lem2  45594  sumnnodd  45639  climlimsupcex  45778  cnrefiisplem  45838  stoweidlem1  46010  stoweidlem5  46014  stoweidlem7  46016  dirkercncflem1  46112  dirkercncflem4  46115  fourierdlem30  46146  fourierdlem42  46158  fourierdlem48  46163  fourierdlem62  46177  fourierdlem63  46178  fourierdlem68  46183  fourierdlem79  46194  sqwvfoura  46237  etransclem32  46275  hoidmvlelem2  46605  iunhoiioolem  46684  vonioolem1  46689  pimdecfgtioo  46726  pimincfltioo  46727  smfmullem1  46800  2ltceilhalf  47337  rehalfge1  47344  m1modnep2mod  47361  fmtnoge3  47524  fmtnoprmfac2lem1  47560  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem4a  47602  proththdlem  47607  stgoldbwt  47770  sgoldbeven3prm  47777  mogoldbb  47779  evengpop3  47792  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  lindslinindimp2lem3  48416  fllogbd  48520  nnolog2flm1  48550