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

Theorem syl5eqbr 4613
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 2610 . 2 𝐶 = 𝐶
41, 2, 33brtr4g 4612 1 (𝜑𝐴𝑅𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475   class class class wbr 4578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579
This theorem is referenced by:  xp1en  7909  map2xp  7993  1sdom  8026  sucxpdom  8032  sniffsupp  8176  wdomima2g  8352  pwsdompw  8887  infunsdom1  8896  infunsdom  8897  infxp  8898  ackbij1lem5  8907  hsmexlem4  9112  imadomg  9215  unidom  9222  unictb  9254  pwcdandom  9346  distrnq  9640  supxrmnf  11978  xov1plusxeqvd  12148  quoremz  12474  quoremnn0ALT  12476  intfrac2  12477  m1modge3gt1  12537  bernneq2  12811  faclbnd4lem1  12900  sqrlem4  13783  reccn2  14124  caucvg  14206  o1fsum  14335  infcvgaux2i  14378  eirrlem  14720  rpnnen2lem12  14742  ruclem12  14758  nno  14885  divalglem5  14907  bitsfzolem  14943  bitsinv1lem  14950  bezoutlem3  15045  lcmfunsnlem  15141  coprmproddvds  15164  oddprmge3  15199  sqnprm  15201  prmreclem6  15412  4sqlem6  15434  4sqlem13  15448  4sqlem16  15451  4sqlem17  15452  2expltfac  15586  odcau  17791  sylow3  17820  efginvrel2  17912  lt6abl  18068  ablfac1lem  18239  evlslem2  19282  gzrngunitlem  19579  zringlpirlem3  19602  znfld  19676  chfacffsupp  20428  cpmidpmatlem3  20444  cctop  20568  csdfil  21456  xpsdsval  21944  nrginvrcnlem  22253  icccmplem2  22382  reconnlem2  22386  iscmet3lem3  22841  minveclem2  22950  minveclem4  22956  ivthlem2  22973  ivthlem3  22974  ovolunlem1a  23016  ovolfiniun  23021  ovoliunlem3  23024  ovoliun  23025  ovolicc2lem4  23040  unmbl  23057  ioombl1lem4  23081  itg2mono  23271  ibladdlem  23337  iblabsr  23347  iblmulc2  23348  dvferm1lem  23496  dvferm2lem  23498  lhop1lem  23525  dvcvx  23532  ftc1a  23549  plyeq0lem  23715  aannenlem3  23834  geolim3  23843  psercnlem1  23928  pserdvlem2  23931  reeff1olem  23949  pilem2  23955  pilem3  23956  cosq14gt0  24011  cosq14ge0  24012  cosne0  24025  recosf1o  24030  resinf1o  24031  argregt0  24105  logcnlem3  24135  logcnlem4  24136  logf1o2  24141  cxpcn3lem  24233  ang180lem2  24285  acosbnd  24372  atanbndlem  24397  leibpi  24414  cxp2lim  24448  emcllem2  24468  ftalem5  24548  basellem9  24560  vmage0  24592  chpge0  24597  chtub  24682  mersenne  24697  bposlem2  24755  bposlem5  24758  bposlem6  24759  bposlem9  24762  gausslemma2dlem0c  24828  gausslemma2dlem0e  24830  lgseisenlem1  24845  lgsquadlem1  24850  lgsquadlem2  24851  lgsquadlem3  24852  chebbnd1lem1  24903  chebbnd1lem2  24904  chebbnd1lem3  24905  mulog2sumlem2  24969  pntpbnd1a  25019  pntibndlem1  25023  pntibndlem3  25026  pntlemc  25029  ostth2  25071  ostth3  25072  smcnlem  26730  minvecolem2  26909  minvecolem4  26914  strlem5  28292  hstrlem5  28300  abrexdomjm  28523  prct  28669  dya2icoseg  29460  omssubadd  29483  omsmeas  29506  oddpwdc  29537  faclim  30679  faclim2  30681  taupilem1  32138  mblfinlem3  32412  mblfinlem4  32413  ibladdnclem  32430  iblmulc2nc  32439  bddiblnc  32444  abrexdom  32489  dalem3  33762  dalem8  33768  dalem25  33796  dalem27  33797  dalem38  33808  dalem44  33814  dalem54  33824  lhpat3  34144  4atexlemunv  34164  4atexlemtlw  34165  4atexlemc  34167  4atexlemnclw  34168  4atexlemex2  34169  4atexlemcnd  34170  cdleme0b  34311  cdleme0c  34312  cdleme0fN  34317  cdlemeulpq  34319  cdleme01N  34320  cdleme0ex1N  34322  cdleme2  34327  cdleme3b  34328  cdleme3c  34329  cdleme3g  34333  cdleme3h  34334  cdleme4a  34338  cdleme7aa  34341  cdleme7c  34344  cdleme7d  34345  cdleme7e  34346  cdleme9  34352  cdleme11fN  34363  cdleme11k  34367  cdleme15d  34376  cdlemednpq  34398  cdleme19c  34405  cdleme20aN  34409  cdleme20e  34413  cdleme21c  34427  cdleme21ct  34429  cdleme22e  34444  cdleme22eALTN  34445  cdleme22f  34446  cdleme23a  34449  cdleme28a  34470  cdleme35f  34554  cdlemeg46frv  34625  cdlemeg46rgv  34628  cdlemeg46req  34629  cdlemg2fv2  34700  cdlemg2m  34704  cdlemg6c  34720  cdlemg31a  34797  cdlemg31b  34798  cdlemk10  34943  cdlemk37  35014  dia2dimlem1  35165  dihjatcclem4  35522  irrapxlem3  36200  pell14qrgapw  36252  dgrsub2  36518  radcnvrat  37329  ressiooinf  38425  fmul01  38441  fmul01lt1lem1  38445  fmul01lt1lem2  38446  sumnnodd  38491  stoweidlem1  38688  stoweidlem5  38692  stoweidlem7  38694  dirkercncflem1  38790  dirkercncflem4  38793  fourierdlem30  38824  fourierdlem42  38836  fourierdlem48  38841  fourierdlem62  38855  fourierdlem63  38856  fourierdlem68  38861  fourierdlem79  38872  sqwvfoura  38915  etransclem32  38953  hoidmvlelem2  39280  iunhoiioolem  39360  vonioolem1  39365  pimdecfgtioo  39398  pimincfltioo  39399  smfmullem1  39470  fmtnoge3  39775  fmtnoprmfac2lem1  39811  sfprmdvdsmersenne  39853  lighneallem2  39856  lighneallem4a  39858  proththdlem  39863  stgoldbwt  39993  evengpop3  40009  bgoldbtbndlem2  40017  bgoldbtbndlem3  40018  pthdlem1  40964  lindslinindimp2lem3  42035  fllogbd  42144  nnolog2flm1  42174
  Copyright terms: Public domain W3C validator