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

Theorem eqbrtrid 5097
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 2825 . 2 𝐶 = 𝐶
41, 2, 33brtr4g 5096 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530   class class class wbr 5062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063
This theorem is referenced by:  map1  8584  xp1en  8595  map2xp  8679  1sdom  8713  sucxpdom  8719  sniffsupp  8865  wdomima2g  9042  endjudisj  9586  dju1dif  9590  mapdjuen  9598  djuxpdom  9603  djufi  9604  pwsdompw  9618  infunsdom1  9627  infunsdom  9628  infxp  9629  ackbij1lem5  9638  hsmexlem4  9843  imadomg  9948  unidom  9957  unictb  9989  pwxpndom2  10079  pwdjundom  10081  distrnq  10375  nnne0  11663  supxrmnf  12703  xov1plusxeqvd  12877  quoremz  13216  quoremnn0ALT  13218  intfrac2  13219  m1modge3gt1  13279  bernneq2  13584  faclbnd4lem1  13646  sqrlem4  14598  reccn2  14946  caucvg  15028  o1fsum  15160  infcvgaux2i  15205  eirrlem  15549  rpnnen2lem12  15570  ruclem12  15586  nno  15725  divalglem5  15740  bitsfzolem  15775  bitsinv1lem  15782  bezoutlem3  15881  lcmfunsnlem  15977  coprmproddvds  15999  oddprmge3  16036  ge2nprmge4  16037  sqnprm  16038  prmreclem6  16249  4sqlem6  16271  4sqlem13  16285  4sqlem16  16288  4sqlem17  16289  2expltfac  16418  odcau  18651  sylow3  18680  efginvrel2  18775  lt6abl  18937  ablfac1lem  19112  evlslem2  20212  gzrngunitlem  20528  zringlpirlem3  20551  znfld  20625  chfacffsupp  21382  cpmidpmatlem3  21398  cctop  21532  csdfil  22420  xpsdsval  22908  nrginvrcnlem  23217  icccmplem2  23348  reconnlem2  23352  iscmet3lem3  23810  minveclem2  23946  minveclem4  23952  ivthlem2  23970  ivthlem3  23971  ovolunlem1a  24014  ovolfiniun  24019  ovoliunlem3  24022  ovoliun  24023  ovolicc2lem4  24038  unmbl  24055  ioombl1lem4  24079  itg2mono  24271  ibladdlem  24337  iblabsr  24347  iblmulc2  24348  dvferm1lem  24498  dvferm2lem  24500  lhop1lem  24527  dvcvx  24534  ftc1a  24551  plyeq0lem  24717  aannenlem3  24836  geolim3  24845  psercnlem1  24930  pserdvlem2  24933  reeff1olem  24951  pilem2  24957  pilem3  24958  cosq14gt0  25013  cosq14ge0  25014  cosne0  25029  recosf1o  25034  resinf1o  25035  argregt0  25108  logcnlem3  25142  logcnlem4  25143  logf1o2  25148  cxpcn3lem  25243  ang180lem2  25303  acosbnd  25393  atanbndlem  25418  leibpi  25436  cxp2lim  25470  emcllem2  25490  ftalem5  25570  basellem9  25582  vmage0  25614  chpge0  25619  chtub  25704  mersenne  25719  bposlem2  25777  bposlem5  25780  bposlem6  25781  bposlem9  25784  gausslemma2dlem0c  25850  gausslemma2dlem0e  25852  lgseisenlem1  25867  lgsquadlem1  25872  lgsquadlem2  25873  lgsquadlem3  25874  chebbnd1lem1  25961  chebbnd1lem2  25962  chebbnd1lem3  25963  mulog2sumlem2  26027  pntpbnd1a  26077  pntibndlem1  26081  pntibndlem3  26084  pntlemc  26087  ostth2  26129  ostth3  26130  pthdlem1  27463  numclwlk1lem2  28065  smcnlem  28390  minvecolem2  28568  minvecolem4  28573  strlem5  29948  hstrlem5  29956  abrexdomjm  30183  prct  30365  cyc3conja  30715  dvdschrmulg  30774  dya2icoseg  31423  omssubadd  31446  omsmeas  31469  oddpwdc  31500  logdivsqrle  31809  faclim  32864  faclim2  32866  taupilem1  34473  mblfinlem3  34800  mblfinlem4  34801  ibladdnclem  34817  iblmulc2nc  34826  bddiblnc  34831  abrexdom  34875  dalem3  36669  dalem8  36675  dalem25  36703  dalem27  36704  dalem38  36715  dalem44  36721  dalem54  36731  lhpat3  37051  4atexlemunv  37071  4atexlemtlw  37072  4atexlemc  37074  4atexlemnclw  37075  4atexlemex2  37076  4atexlemcnd  37077  cdleme0b  37217  cdleme0c  37218  cdleme0fN  37223  cdlemeulpq  37225  cdleme01N  37226  cdleme0ex1N  37228  cdleme2  37233  cdleme3b  37234  cdleme3c  37235  cdleme3g  37239  cdleme3h  37240  cdleme4a  37244  cdleme7aa  37247  cdleme7c  37250  cdleme7d  37251  cdleme7e  37252  cdleme9  37258  cdleme11fN  37269  cdleme11k  37273  cdleme15d  37282  cdlemednpq  37304  cdleme19c  37310  cdleme20aN  37314  cdleme20e  37318  cdleme21c  37332  cdleme21ct  37334  cdleme22e  37349  cdleme22eALTN  37350  cdleme22f  37351  cdleme23a  37354  cdleme28a  37375  cdleme35f  37459  cdlemeg46frv  37530  cdlemeg46rgv  37533  cdlemeg46req  37534  cdlemg2fv2  37605  cdlemg2m  37609  cdlemg6c  37625  cdlemg31a  37702  cdlemg31b  37703  cdlemk10  37848  cdlemk37  37919  dia2dimlem1  38069  dihjatcclem4  38426  3cubeslem1  39148  irrapxlem3  39288  pell14qrgapw  39340  dgrsub2  39602  radcnvrat  40513  ressiooinf  41700  fmul01  41728  fmul01lt1lem1  41732  fmul01lt1lem2  41733  sumnnodd  41778  climlimsupcex  41917  cnrefiisplem  41977  stoweidlem1  42154  stoweidlem5  42158  stoweidlem7  42160  dirkercncflem1  42256  dirkercncflem4  42259  fourierdlem30  42290  fourierdlem42  42302  fourierdlem48  42307  fourierdlem62  42321  fourierdlem63  42322  fourierdlem68  42327  fourierdlem79  42338  sqwvfoura  42381  etransclem32  42419  hoidmvlelem2  42746  iunhoiioolem  42825  vonioolem1  42830  pimdecfgtioo  42863  pimincfltioo  42864  smfmullem1  42934  fmtnoge3  43526  fmtnoprmfac2lem1  43562  sfprmdvdsmersenne  43602  lighneallem2  43605  lighneallem4a  43607  proththdlem  43612  stgoldbwt  43775  sgoldbeven3prm  43782  mogoldbb  43784  evengpop3  43797  bgoldbtbndlem2  43805  bgoldbtbndlem3  43806  lindslinindimp2lem3  44349  fllogbd  44454  nnolog2flm1  44484
  Copyright terms: Public domain W3C validator