Theorem eqbrtrid 5178

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144

This theorem is referenced by:  map1  9059  xp1en  9076  map2xp  9166  rex2dom  9265  1sdomOLD  9268  sucxpdom  9274  sniffsupp  9418  wdomima2g  9604  endjudisj  10186  dju1dif  10190  mapdjuen  10198  djuxpdom  10203  djufi  10204  pwsdompw  10222  infunsdom1  10231  infunsdom  10232  infxp  10233  ackbij1lem5  10242  hsmexlem4  10447  imadomg  10552  unidom  10561  unictb  10593  pwxpndom2  10683  pwdjundom  10685  distrnq  10979  nnne0  12271  supxrmnf  13323  xov1plusxeqvd  13502  quoremz  13847  quoremnn0ALT  13849  intfrac2  13850  m1modge3gt1  13910  bernneq2  14219  faclbnd4lem1  14279  01sqrexlem4  15219  reccn2  15568  caucvg  15652  o1fsum  15786  infcvgaux2i  15831  eirrlem  16175  rpnnen2lem12  16196  ruclem12  16212  nno  16353  divalglem5  16368  bitsfzolem  16403  bitsinv1lem  16410  bezoutlem3  16511  lcmfunsnlem  16606  coprmproddvds  16628  oddprmge3  16665  ge2nprmge4  16666  sqnprm  16667  prmreclem6  16884  4sqlem6  16906  4sqlem13  16920  4sqlem16  16923  4sqlem17  16924  2expltfac  17056  odcau  19553  sylow3  19582  efginvrel2  19676  lt6abl  19844  ablfac1lem  20019  gzrngunitlem  21359  zringlpirlem3  21384  dvdschrmulg  21452  znfld  21488  evlslem2  22019  chfacffsupp  22752  cpmidpmatlem3  22768  cctop  22903  csdfil  23792  xpsdsval  24281  nrginvrcnlem  24602  icccmplem2  24733  reconnlem2  24737  iscmet3lem3  25212  minveclem2  25348  minveclem4  25354  ivthlem2  25375  ivthlem3  25376  ovolunlem1a  25419  ovolfiniun  25424  ovoliunlem3  25427  ovoliun  25428  ovolicc2lem4  25443  unmbl  25460  ioombl1lem4  25484  itg2mono  25677  ibladdlem  25743  iblabsr  25753  iblmulc2  25754  bddiblnc  25765  dvferm1lem  25910  dvferm2lem  25912  lhop1lem  25940  dvcvx  25947  ftc1a  25966  plyeq0lem  26138  aannenlem3  26259  geolim3  26268  psercnlem1  26356  pserdvlem2  26359  reeff1olem  26377  pilem2  26383  pilem3  26384  cosq14gt0  26439  cosq14ge0  26440  cosne0  26457  recosf1o  26463  resinf1o  26464  argregt0  26538  logcnlem3  26572  logcnlem4  26573  logf1o2  26578  cxpcn3lem  26676  ang180lem2  26736  acosbnd  26826  atanbndlem  26851  leibpi  26868  cxp2lim  26903  emcllem2  26923  ftalem5  27003  basellem9  27015  vmage0  27047  chpge0  27052  chtub  27139  mersenne  27154  bposlem2  27212  bposlem5  27215  bposlem6  27216  bposlem9  27219  gausslemma2dlem0c  27285  gausslemma2dlem0e  27287  lgseisenlem1  27302  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  chebbnd1lem1  27396  chebbnd1lem2  27397  chebbnd1lem3  27398  mulog2sumlem2  27462  pntpbnd1a  27512  pntibndlem1  27516  pntibndlem3  27519  pntlemc  27522  ostth2  27564  ostth3  27565  absmuls  28132  pthdlem1  29574  numclwlk1lem2  30174  smcnlem  30501  minvecolem2  30679  minvecolem4  30684  strlem5  32059  hstrlem5  32067  abrexdomjm  32296  prct  32491  cyc3conja  32873  prmidl0  33161  dya2icoseg  33892  omssubadd  33915  omsmeas  33938  oddpwdc  33969  logdivsqrle  34277  faclim  35335  faclim2  35337  taupilem1  36795  mblfinlem3  37127  mblfinlem4  37128  ibladdnclem  37144  iblmulc2nc  37153  abrexdom  37198  dalem3  39132  dalem8  39138  dalem25  39166  dalem27  39167  dalem38  39178  dalem44  39184  dalem54  39194  lhpat3  39514  4atexlemunv  39534  4atexlemtlw  39535  4atexlemc  39537  4atexlemnclw  39538  4atexlemex2  39539  4atexlemcnd  39540  cdleme0b  39680  cdleme0c  39681  cdleme0fN  39686  cdlemeulpq  39688  cdleme01N  39689  cdleme0ex1N  39691  cdleme2  39696  cdleme3b  39697  cdleme3c  39698  cdleme3g  39702  cdleme3h  39703  cdleme4a  39707  cdleme7aa  39710  cdleme7c  39713  cdleme7d  39714  cdleme7e  39715  cdleme9  39721  cdleme11fN  39732  cdleme11k  39736  cdleme15d  39745  cdlemednpq  39767  cdleme19c  39773  cdleme20aN  39777  cdleme20e  39781  cdleme21c  39795  cdleme21ct  39797  cdleme22e  39812  cdleme22eALTN  39813  cdleme22f  39814  cdleme23a  39817  cdleme28a  39838  cdleme35f  39922  cdlemeg46frv  39993  cdlemeg46rgv  39996  cdlemeg46req  39997  cdlemg2fv2  40068  cdlemg2m  40072  cdlemg6c  40088  cdlemg31a  40165  cdlemg31b  40166  cdlemk10  40311  cdlemk37  40382  dia2dimlem1  40532  dihjatcclem4  40889  imadomfi  41468  metakunt30  41677  3cubeslem1  42095  irrapxlem3  42235  pell14qrgapw  42287  dgrsub2  42550  radcnvrat  43742  ressiooinf  44933  fmul01  44959  fmul01lt1lem1  44963  fmul01lt1lem2  44964  sumnnodd  45009  climlimsupcex  45148  cnrefiisplem  45208  stoweidlem1  45380  stoweidlem5  45384  stoweidlem7  45386  dirkercncflem1  45482  dirkercncflem4  45485  fourierdlem30  45516  fourierdlem42  45528  fourierdlem48  45533  fourierdlem62  45547  fourierdlem63  45548  fourierdlem68  45553  fourierdlem79  45564  sqwvfoura  45607  etransclem32  45645  hoidmvlelem2  45975  iunhoiioolem  46054  vonioolem1  46059  pimdecfgtioo  46096  pimincfltioo  46097  smfmullem1  46170  fmtnoge3  46861  fmtnoprmfac2lem1  46897  sfprmdvdsmersenne  46934  lighneallem2  46937  lighneallem4a  46939  proththdlem  46944  stgoldbwt  47107  sgoldbeven3prm  47114  mogoldbb  47116  evengpop3  47129  bgoldbtbndlem2  47137  bgoldbtbndlem3  47138  lindslinindimp2lem3  47519  fllogbd  47624  nnolog2flm1  47654