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

Theorem syl5eqbr 4879
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl5eqbr.1 𝐴 = 𝐵
syl5eqbr.2 (𝜑𝐵𝑅𝐶)
Assertion
Ref Expression
syl5eqbr (𝜑𝐴𝑅𝐶)

Proof of Theorem syl5eqbr
StepHypRef Expression
1 syl5eqbr.2 . 2 (𝜑𝐵𝑅𝐶)
2 syl5eqbr.1 . 2 𝐴 = 𝐵
3 eqid 2806 . 2 𝐶 = 𝐶
41, 2, 33brtr4g 4878 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637   class class class wbr 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845
This theorem is referenced by:  map1  8271  xp1en  8281  map2xp  8365  1sdom  8398  sucxpdom  8404  sniffsupp  8550  wdomima2g  8726  pwsdompw  9307  infunsdom1  9316  infunsdom  9317  infxp  9318  ackbij1lem5  9327  hsmexlem4  9532  imadomg  9637  unidom  9646  unictb  9678  pwxpndom2  9768  pwcdandom  9770  distrnq  10064  supxrmnf  12361  xov1plusxeqvd  12537  quoremz  12874  quoremnn0ALT  12876  intfrac2  12877  m1modge3gt1  12937  bernneq2  13210  faclbnd4lem1  13296  sqrlem4  14205  reccn2  14546  caucvg  14628  o1fsum  14763  infcvgaux2i  14808  eirrlem  15148  rpnnen2lem12  15170  ruclem12  15186  nno  15314  divalglem5  15336  bitsfzolem  15371  bitsinv1lem  15378  bezoutlem3  15473  lcmfunsnlem  15569  coprmproddvds  15591  oddprmge3  15626  sqnprm  15627  prmreclem6  15838  4sqlem6  15860  4sqlem13  15874  4sqlem16  15877  4sqlem17  15878  2expltfac  16007  odcau  18216  sylow3  18245  efginvrel2  18337  lt6abl  18493  ablfac1lem  18665  evlslem2  19716  gzrngunitlem  20015  zringlpirlem3  20038  znfld  20112  chfacffsupp  20871  cpmidpmatlem3  20887  cctop  21021  csdfil  21908  xpsdsval  22396  nrginvrcnlem  22705  icccmplem2  22836  reconnlem2  22840  iscmet3lem3  23298  minveclem2  23408  minveclem4  23414  ivthlem2  23432  ivthlem3  23433  ovolunlem1a  23476  ovolfiniun  23481  ovoliunlem3  23484  ovoliun  23485  ovolicc2lem4  23500  unmbl  23517  ioombl1lem4  23541  itg2mono  23733  ibladdlem  23799  iblabsr  23809  iblmulc2  23810  dvferm1lem  23960  dvferm2lem  23962  lhop1lem  23989  dvcvx  23996  ftc1a  24013  plyeq0lem  24179  aannenlem3  24298  geolim3  24307  psercnlem1  24392  pserdvlem2  24395  reeff1olem  24413  pilem2  24419  pilem3  24420  pilem3OLD  24421  cosq14gt0  24476  cosq14ge0  24477  cosne0  24490  recosf1o  24495  resinf1o  24496  argregt0  24569  logcnlem3  24603  logcnlem4  24604  logf1o2  24609  cxpcn3lem  24701  ang180lem2  24753  acosbnd  24840  atanbndlem  24865  leibpi  24882  cxp2lim  24916  emcllem2  24936  ftalem5  25016  basellem9  25028  vmage0  25060  chpge0  25065  chtub  25150  mersenne  25165  bposlem2  25223  bposlem5  25226  bposlem6  25227  bposlem9  25230  gausslemma2dlem0c  25296  gausslemma2dlem0e  25298  lgseisenlem1  25313  lgsquadlem1  25318  lgsquadlem2  25319  lgsquadlem3  25320  chebbnd1lem1  25371  chebbnd1lem2  25372  chebbnd1lem3  25373  mulog2sumlem2  25437  pntpbnd1a  25487  pntibndlem1  25491  pntibndlem3  25494  pntlemc  25497  ostth2  25539  ostth3  25540  pthdlem1  26889  numclwlk1lem2  27549  smcnlem  27879  minvecolem2  28058  minvecolem4  28063  strlem5  29441  hstrlem5  29449  abrexdomjm  29669  prct  29818  dya2icoseg  30663  omssubadd  30686  omsmeas  30709  oddpwdc  30740  logdivsqrle  31052  faclim  31952  faclim2  31954  taupilem1  33482  mblfinlem3  33759  mblfinlem4  33760  ibladdnclem  33776  iblmulc2nc  33785  bddiblnc  33790  abrexdom  33835  dalem3  35442  dalem8  35448  dalem25  35476  dalem27  35477  dalem38  35488  dalem44  35494  dalem54  35504  lhpat3  35824  4atexlemunv  35844  4atexlemtlw  35845  4atexlemc  35847  4atexlemnclw  35848  4atexlemex2  35849  4atexlemcnd  35850  cdleme0b  35990  cdleme0c  35991  cdleme0fN  35996  cdlemeulpq  35998  cdleme01N  35999  cdleme0ex1N  36001  cdleme2  36006  cdleme3b  36007  cdleme3c  36008  cdleme3g  36012  cdleme3h  36013  cdleme4a  36017  cdleme7aa  36020  cdleme7c  36023  cdleme7d  36024  cdleme7e  36025  cdleme9  36031  cdleme11fN  36042  cdleme11k  36046  cdleme15d  36055  cdlemednpq  36077  cdleme19c  36083  cdleme20aN  36087  cdleme20e  36091  cdleme21c  36105  cdleme21ct  36107  cdleme22e  36122  cdleme22eALTN  36123  cdleme22f  36124  cdleme23a  36127  cdleme28a  36148  cdleme35f  36232  cdlemeg46frv  36303  cdlemeg46rgv  36306  cdlemeg46req  36307  cdlemg2fv2  36378  cdlemg2m  36382  cdlemg6c  36398  cdlemg31a  36475  cdlemg31b  36476  cdlemk10  36621  cdlemk37  36692  dia2dimlem1  36842  dihjatcclem4  37199  irrapxlem3  37887  pell14qrgapw  37939  dgrsub2  38203  radcnvrat  39010  ressiooinf  40261  fmul01  40289  fmul01lt1lem1  40293  fmul01lt1lem2  40294  sumnnodd  40339  climlimsupcex  40478  cnrefiisplem  40532  stoweidlem1  40694  stoweidlem5  40698  stoweidlem7  40700  dirkercncflem1  40796  dirkercncflem4  40799  fourierdlem30  40830  fourierdlem42  40842  fourierdlem48  40847  fourierdlem62  40861  fourierdlem63  40862  fourierdlem68  40867  fourierdlem79  40878  sqwvfoura  40921  etransclem32  40959  hoidmvlelem2  41289  iunhoiioolem  41368  vonioolem1  41373  pimdecfgtioo  41406  pimincfltioo  41407  smfmullem1  41477  fmtnoge3  42014  fmtnoprmfac2lem1  42050  sfprmdvdsmersenne  42092  lighneallem2  42095  lighneallem4a  42097  proththdlem  42102  stgoldbwt  42236  sgoldbeven3prm  42243  mogoldbb  42245  evengpop3  42258  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  lindslinindimp2lem3  42814  fllogbd  42919  nnolog2flm1  42949
  Copyright terms: Public domain W3C validator