MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqbrtrid Structured version   Visualization version   GIF version

Theorem eqbrtrid 5141
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
StepHypRef Expression
1 eqbrtrid.2 . 2 (𝜑𝐵𝑅𝐶)
2 eqbrtrid.1 . 2 𝐴 = 𝐵
3 eqid 2737 . 2 𝐶 = 𝐶
41, 2, 33brtr4g 5140 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542   class class class wbr 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107
This theorem is referenced by:  map1  8985  xp1en  9002  map2xp  9092  rex2dom  9191  1sdomOLD  9194  sucxpdom  9200  sniffsupp  9337  wdomima2g  9523  endjudisj  10105  dju1dif  10109  mapdjuen  10117  djuxpdom  10122  djufi  10123  pwsdompw  10141  infunsdom1  10150  infunsdom  10151  infxp  10152  ackbij1lem5  10161  hsmexlem4  10366  imadomg  10471  unidom  10480  unictb  10512  pwxpndom2  10602  pwdjundom  10604  distrnq  10898  nnne0  12188  supxrmnf  13237  xov1plusxeqvd  13416  quoremz  13761  quoremnn0ALT  13763  intfrac2  13764  m1modge3gt1  13824  bernneq2  14134  faclbnd4lem1  14194  01sqrexlem4  15131  reccn2  15480  caucvg  15564  o1fsum  15699  infcvgaux2i  15744  eirrlem  16087  rpnnen2lem12  16108  ruclem12  16124  nno  16265  divalglem5  16280  bitsfzolem  16315  bitsinv1lem  16322  bezoutlem3  16423  lcmfunsnlem  16518  coprmproddvds  16540  oddprmge3  16577  ge2nprmge4  16578  sqnprm  16579  prmreclem6  16794  4sqlem6  16816  4sqlem13  16830  4sqlem16  16833  4sqlem17  16834  2expltfac  16966  odcau  19387  sylow3  19416  efginvrel2  19510  lt6abl  19673  ablfac1lem  19848  gzrngunitlem  20865  zringlpirlem3  20888  znfld  20970  evlslem2  21492  chfacffsupp  22208  cpmidpmatlem3  22224  cctop  22359  csdfil  23248  xpsdsval  23737  nrginvrcnlem  24058  icccmplem2  24189  reconnlem2  24193  iscmet3lem3  24657  minveclem2  24793  minveclem4  24799  ivthlem2  24819  ivthlem3  24820  ovolunlem1a  24863  ovolfiniun  24868  ovoliunlem3  24871  ovoliun  24872  ovolicc2lem4  24887  unmbl  24904  ioombl1lem4  24928  itg2mono  25121  ibladdlem  25187  iblabsr  25197  iblmulc2  25198  bddiblnc  25209  dvferm1lem  25351  dvferm2lem  25353  lhop1lem  25380  dvcvx  25387  ftc1a  25404  plyeq0lem  25574  aannenlem3  25693  geolim3  25702  psercnlem1  25787  pserdvlem2  25790  reeff1olem  25808  pilem2  25814  pilem3  25815  cosq14gt0  25870  cosq14ge0  25871  cosne0  25888  recosf1o  25894  resinf1o  25895  argregt0  25968  logcnlem3  26002  logcnlem4  26003  logf1o2  26008  cxpcn3lem  26103  ang180lem2  26163  acosbnd  26253  atanbndlem  26278  leibpi  26295  cxp2lim  26329  emcllem2  26349  ftalem5  26429  basellem9  26441  vmage0  26473  chpge0  26478  chtub  26563  mersenne  26578  bposlem2  26636  bposlem5  26639  bposlem6  26640  bposlem9  26643  gausslemma2dlem0c  26709  gausslemma2dlem0e  26711  lgseisenlem1  26726  lgsquadlem1  26731  lgsquadlem2  26732  lgsquadlem3  26733  chebbnd1lem1  26820  chebbnd1lem2  26821  chebbnd1lem3  26822  mulog2sumlem2  26886  pntpbnd1a  26936  pntibndlem1  26940  pntibndlem3  26943  pntlemc  26946  ostth2  26988  ostth3  26989  pthdlem1  28717  numclwlk1lem2  29317  smcnlem  29642  minvecolem2  29820  minvecolem4  29825  strlem5  31200  hstrlem5  31208  abrexdomjm  31436  prct  31634  cyc3conja  32009  dvdschrmulg  32069  prmidl0  32226  dya2icoseg  32880  omssubadd  32903  omsmeas  32926  oddpwdc  32957  logdivsqrle  33266  faclim  34322  faclim2  34324  taupilem1  35795  mblfinlem3  36120  mblfinlem4  36121  ibladdnclem  36137  iblmulc2nc  36146  abrexdom  36192  dalem3  38130  dalem8  38136  dalem25  38164  dalem27  38165  dalem38  38176  dalem44  38182  dalem54  38192  lhpat3  38512  4atexlemunv  38532  4atexlemtlw  38533  4atexlemc  38535  4atexlemnclw  38536  4atexlemex2  38537  4atexlemcnd  38538  cdleme0b  38678  cdleme0c  38679  cdleme0fN  38684  cdlemeulpq  38686  cdleme01N  38687  cdleme0ex1N  38689  cdleme2  38694  cdleme3b  38695  cdleme3c  38696  cdleme3g  38700  cdleme3h  38701  cdleme4a  38705  cdleme7aa  38708  cdleme7c  38711  cdleme7d  38712  cdleme7e  38713  cdleme9  38719  cdleme11fN  38730  cdleme11k  38734  cdleme15d  38743  cdlemednpq  38765  cdleme19c  38771  cdleme20aN  38775  cdleme20e  38779  cdleme21c  38793  cdleme21ct  38795  cdleme22e  38810  cdleme22eALTN  38811  cdleme22f  38812  cdleme23a  38815  cdleme28a  38836  cdleme35f  38920  cdlemeg46frv  38991  cdlemeg46rgv  38994  cdlemeg46req  38995  cdlemg2fv2  39066  cdlemg2m  39070  cdlemg6c  39086  cdlemg31a  39163  cdlemg31b  39164  cdlemk10  39309  cdlemk37  39380  dia2dimlem1  39530  dihjatcclem4  39887  metakunt30  40609  3cubeslem1  41010  irrapxlem3  41150  pell14qrgapw  41202  dgrsub2  41465  radcnvrat  42601  ressiooinf  43802  fmul01  43828  fmul01lt1lem1  43832  fmul01lt1lem2  43833  sumnnodd  43878  climlimsupcex  44017  cnrefiisplem  44077  stoweidlem1  44249  stoweidlem5  44253  stoweidlem7  44255  dirkercncflem1  44351  dirkercncflem4  44354  fourierdlem30  44385  fourierdlem42  44397  fourierdlem48  44402  fourierdlem62  44416  fourierdlem63  44417  fourierdlem68  44422  fourierdlem79  44433  sqwvfoura  44476  etransclem32  44514  hoidmvlelem2  44844  iunhoiioolem  44923  vonioolem1  44928  pimdecfgtioo  44965  pimincfltioo  44966  smfmullem1  45039  fmtnoge3  45729  fmtnoprmfac2lem1  45765  sfprmdvdsmersenne  45802  lighneallem2  45805  lighneallem4a  45807  proththdlem  45812  stgoldbwt  45975  sgoldbeven3prm  45982  mogoldbb  45984  evengpop3  45997  bgoldbtbndlem2  46005  bgoldbtbndlem3  46006  lindslinindimp2lem3  46548  fllogbd  46653  nnolog2flm1  46683
  Copyright terms: Public domain W3C validator