Theorem eqbrtrid 5114

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080

This theorem is referenced by:  map1  8984  xp1en  8998  map2xp  9082  rex2dom  9160  sucxpdom  9168  sniffsupp  9310  wdomima2g  9498  endjudisj  10089  dju1dif  10093  mapdjuen  10101  djuxpdom  10106  djufi  10107  pwsdompw  10123  infunsdom1  10132  infunsdom  10133  infxp  10134  ackbij1lem5  10143  hsmexlem4  10349  imadomg  10454  unidom  10463  unictb  10496  pwxpndom2  10586  pwdjundom  10588  distrnq  10882  nnne0  12209  supxrmnf  13267  xov1plusxeqvd  13449  quoremz  13812  quoremnn0ALT  13814  intfrac2  13815  m1modge3gt1  13878  bernneq2  14190  faclbnd4lem1  14253  01sqrexlem4  15205  reccn2  15557  caucvg  15639  o1fsum  15774  infcvgaux2i  15821  eirrlem  16169  rpnnen2lem12  16190  ruclem12  16206  nno  16349  divalglem5  16364  bitsfzolem  16401  bitsinv1lem  16408  bezoutlem3  16508  lcmfunsnlem  16608  coprmproddvds  16630  oddprmge3  16668  ge2nprmge4  16669  sqnprm  16670  prmreclem6  16890  4sqlem6  16912  4sqlem13  16926  4sqlem16  16929  4sqlem17  16930  2expltfac  17061  odcau  19577  sylow3  19606  efginvrel2  19700  lt6abl  19868  ablfac1lem  20043  gzrngunitlem  21414  zringlpirlem3  21446  dvdschrmulg  21510  znfld  21542  evlslem2  22062  chfacffsupp  22846  cpmidpmatlem3  22862  cctop  22996  csdfil  23884  xpsdsval  24371  nrginvrcnlem  24681  icccmplem2  24814  reconnlem2  24818  iscmet3lem3  25282  minveclem2  25418  minveclem4  25424  ivthlem2  25444  ivthlem3  25445  ovolunlem1a  25488  ovolfiniun  25493  ovoliunlem3  25496  ovoliun  25497  ovolicc2lem4  25512  unmbl  25529  ioombl1lem4  25553  itg2mono  25745  ibladdlem  25812  iblabsr  25822  iblmulc2  25823  bddiblnc  25834  dvferm1lem  25976  dvferm2lem  25978  lhop1lem  26005  dvcvx  26012  ftc1a  26029  plyeq0lem  26200  aannenlem3  26321  geolim3  26330  psercnlem1  26415  pserdvlem2  26418  reeff1olem  26436  pilem2  26442  pilem3  26443  cosq14gt0  26499  cosq14ge0  26500  cosne0  26518  recosf1o  26524  resinf1o  26525  argregt0  26599  logcnlem3  26633  logcnlem4  26634  logf1o2  26639  cxpcn3lem  26736  ang180lem2  26799  acosbnd  26889  atanbndlem  26914  leibpi  26931  cxp2lim  26965  emcllem2  26985  ftalem5  27065  basellem9  27077  vmage0  27109  chpge0  27114  chtub  27200  mersenne  27215  bposlem2  27273  bposlem5  27276  bposlem6  27277  bposlem9  27280  gausslemma2dlem0c  27346  gausslemma2dlem0e  27348  lgseisenlem1  27363  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  chebbnd1lem1  27457  chebbnd1lem2  27458  chebbnd1lem3  27459  mulog2sumlem2  27523  pntpbnd1a  27573  pntibndlem1  27577  pntibndlem3  27580  pntlemc  27583  ostth2  27625  ostth3  27626  absmuls  28261  pthdlem1  29859  numclwlk1lem2  30465  smcnlem  30793  minvecolem2  30971  minvecolem4  30976  strlem5  32351  hstrlem5  32359  abrexdomjm  32602  prct  32812  cyc3conja  33245  elrgspnlem2  33331  prmidl0  33540  mplvrpmga  33736  psrmonprod  33743  fldextrspunlsplem  33864  constrext2chnlem  33941  dya2icoseg  34468  omssubadd  34491  omsmeas  34514  oddpwdc  34545  logdivsqrle  34841  faclim  35981  faclim2  35983  taupilem1  37688  mblfinlem3  38033  mblfinlem4  38034  ibladdnclem  38050  iblmulc2nc  38059  abrexdom  38104  dalem3  40163  dalem8  40169  dalem25  40197  dalem27  40198  dalem38  40209  dalem44  40215  dalem54  40225  lhpat3  40545  4atexlemunv  40565  4atexlemtlw  40566  4atexlemc  40568  4atexlemnclw  40569  4atexlemex2  40570  4atexlemcnd  40571  cdleme0b  40711  cdleme0c  40712  cdleme0fN  40717  cdlemeulpq  40719  cdleme01N  40720  cdleme0ex1N  40722  cdleme2  40727  cdleme3b  40728  cdleme3c  40729  cdleme3g  40733  cdleme3h  40734  cdleme4a  40738  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme9  40752  cdleme11fN  40763  cdleme11k  40767  cdleme15d  40776  cdlemednpq  40798  cdleme19c  40804  cdleme20aN  40808  cdleme20e  40812  cdleme21c  40826  cdleme21ct  40828  cdleme22e  40843  cdleme22eALTN  40844  cdleme22f  40845  cdleme23a  40848  cdleme28a  40869  cdleme35f  40953  cdlemeg46frv  41024  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemg2fv2  41099  cdlemg2m  41103  cdlemg6c  41119  cdlemg31a  41196  cdlemg31b  41197  cdlemk10  41342  cdlemk37  41413  dia2dimlem1  41563  dihjatcclem4  41920  imadomfi  42494  aks5lem1  42678  3cubeslem1  43140  irrapxlem3  43276  pell14qrgapw  43328  dgrsub2  43587  radcnvrat  44765  ressiooinf  46009  fmul01  46032  fmul01lt1lem1  46036  fmul01lt1lem2  46037  sumnnodd  46082  climlimsupcex  46219  cnrefiisplem  46279  stoweidlem1  46451  stoweidlem5  46455  stoweidlem7  46457  dirkercncflem1  46553  dirkercncflem4  46556  fourierdlem30  46587  fourierdlem42  46599  fourierdlem48  46604  fourierdlem62  46618  fourierdlem63  46619  fourierdlem68  46624  fourierdlem79  46635  sqwvfoura  46678  etransclem32  46716  hoidmvlelem2  47046  iunhoiioolem  47125  vonioolem1  47130  pimdecfgtioo  47167  pimincfltioo  47168  smfmullem1  47241  2ltceilhalf  47802  rehalfge1  47809  m1modnep2mod  47828  difmodm1lt  47835  2timesltsqm1  47849  fmtnoge3  48015  fmtnoprmfac2lem1  48051  sfprmdvdsmersenne  48088  lighneallem2  48091  lighneallem4a  48093  proththdlem  48098  nprmdvdsfacm1lem2  48106  stgoldbwt  48274  sgoldbeven3prm  48281  mogoldbb  48283  evengpop3  48296  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  lindslinindimp2lem3  48958  fllogbd  49058  nnolog2flm1  49088