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

Theorem syl5eqbr 4436
Description: A chained equality inference for a binary relation. (Contributed by NM, 11-Oct-1999.)
Hypotheses
Ref Expression
syl5eqbr.1  |-  A  =  B
syl5eqbr.2  |-  ( ph  ->  B R C )
Assertion
Ref Expression
syl5eqbr  |-  ( ph  ->  A R C )

Proof of Theorem syl5eqbr
StepHypRef Expression
1 syl5eqbr.2 . 2  |-  ( ph  ->  B R C )
2 syl5eqbr.1 . 2  |-  A  =  B
3 eqid 2451 . 2  |-  C  =  C
41, 2, 33brtr4g 4435 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444   class class class wbr 4402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403
This theorem is referenced by:  xp1en  7658  map2xp  7742  1sdom  7775  sucxpdom  7781  sniffsupp  7923  wdomima2g  8101  pwsdompw  8634  infunsdom1  8643  infunsdom  8644  infxp  8645  ackbij1lem5  8654  hsmexlem4  8859  imadomg  8962  unidom  8968  unictb  9000  pwcdandom  9092  distrnq  9386  supxrmnf  11603  xov1plusxeqvd  11778  quoremz  12082  quoremnn0ALT  12084  intfrac2  12085  bernneq2  12399  faclbnd4lem1  12478  sqrlem4  13309  reccn2  13660  caucvg  13745  o1fsum  13873  infcvgaux2i  13916  eirrlem  14256  rpnnen2  14278  ruclem12  14293  divalglem5OLD  14376  divalglem5  14377  bitsfzolem  14407  bitsfzolemOLD  14408  bitsinv1lem  14415  bezoutlem3OLD  14505  bezoutlem3  14508  lcmsledvdsOLD  14585  lcmfunsnlem  14614  sqnprm  14646  coprmproddvds  14680  prmreclem6  14865  4sqlem6  14887  4sqlem13OLD  14901  4sqlem16OLD  14904  4sqlem17OLD  14905  4sqlem13  14907  4sqlem16  14910  4sqlem17  14911  2expltfac  15063  odcau  17256  sylow3  17285  efginvrel2  17377  lt6abl  17529  ablfac1lem  17701  evlslem2  18735  gzrngunitlem  19032  zringlpirlem3OLD  19055  zringlpirlem3  19057  znfld  19131  chfacffsupp  19880  cpmidpmatlem3  19896  cctop  20021  csdfil  20909  xpsdsval  21396  nrginvrcnlem  21693  icccmplem2  21841  reconnlem2  21845  iscmet3lem3  22260  minveclem2  22368  minveclem4  22374  minveclem2OLD  22380  minveclem4OLD  22386  ivthlem2  22403  ivthlem3  22404  ovolunlem1a  22449  ovolfiniun  22454  ovoliunlem3  22457  ovoliun  22458  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  unmbl  22491  ioombl1lem4  22514  itg2mono  22711  ibladdlem  22777  iblabsr  22787  iblmulc2  22788  dvferm1lem  22936  dvferm2lem  22938  lhop1lem  22965  dvcvx  22972  ftc1a  22989  plyeq0lem  23164  aannenlem3  23286  geolim3  23295  psercnlem1  23380  pserdvlem2  23383  reeff1olem  23401  pilem2  23407  pilem2OLD  23408  pilem3  23409  pilem3OLD  23410  cosq14gt0  23465  cosq14ge0  23466  cosne0  23479  recosf1o  23484  resinf1o  23485  argregt0  23559  logcnlem3  23589  logcnlem4  23590  logf1o2  23595  cxpcn3lem  23687  ang180lem2  23739  acosbnd  23826  atanbndlem  23851  leibpi  23868  cxp2lim  23902  emcllem2  23922  ftalem5  24001  ftalem5OLD  24003  basellem9  24015  vmage0  24048  chpge0  24053  chtub  24140  mersenne  24155  bposlem2  24213  bposlem5  24216  bposlem6  24217  bposlem9  24220  lgseisenlem1  24277  lgsquadlem1  24282  lgsquadlem2  24283  lgsquadlem3  24284  chebbnd1lem1  24307  chebbnd1lem2  24308  chebbnd1lem3  24309  mulog2sumlem2  24373  pntpbnd1a  24423  pntibndlem1  24427  pntibndlem3  24430  pntlemc  24433  ostth2  24475  ostth3  24476  smcnlem  26333  minvecolem2  26517  minvecolem4  26522  minvecolem2OLD  26527  minvecolem4OLD  26532  strlem5  27908  hstrlem5  27916  abrexdomjm  28141  prct  28296  dya2icoseg  29099  omssubadd  29128  omssubaddOLD  29132  omsmeas  29155  omsmeasOLD  29156  oddpwdc  29187  faclim  30382  faclim2  30384  taupilem1  31722  mblfinlem3  31979  mblfinlem4  31980  ibladdnclem  31998  iblmulc2nc  32007  bddiblnc  32012  abrexdom  32057  dalem3  33229  dalem8  33235  dalem25  33263  dalem27  33264  dalem38  33275  dalem44  33281  dalem54  33291  lhpat3  33611  4atexlemunv  33631  4atexlemtlw  33632  4atexlemc  33634  4atexlemnclw  33635  4atexlemex2  33636  4atexlemcnd  33637  cdleme0b  33778  cdleme0c  33779  cdleme0fN  33784  cdlemeulpq  33786  cdleme01N  33787  cdleme0ex1N  33789  cdleme2  33794  cdleme3b  33795  cdleme3c  33796  cdleme3g  33800  cdleme3h  33801  cdleme4a  33805  cdleme7aa  33808  cdleme7c  33811  cdleme7d  33812  cdleme7e  33813  cdleme9  33819  cdleme11fN  33830  cdleme11k  33834  cdleme15d  33843  cdlemednpq  33865  cdleme19c  33872  cdleme20aN  33876  cdleme20e  33880  cdleme21c  33894  cdleme21ct  33896  cdleme22e  33911  cdleme22eALTN  33912  cdleme22f  33913  cdleme23a  33916  cdleme28a  33937  cdleme35f  34021  cdlemeg46frv  34092  cdlemeg46rgv  34095  cdlemeg46req  34096  cdlemg2fv2  34167  cdlemg2m  34171  cdlemg6c  34187  cdlemg31a  34264  cdlemg31b  34265  cdlemk10  34410  cdlemk37  34481  dia2dimlem1  34632  dihjatcclem4  34989  irrapxlem3  35668  pell14qrgapw  35722  dgrsub2  35994  radcnvrat  36663  fmul01  37658  fmul01lt1lem1  37662  fmul01lt1lem2  37663  sumnnodd  37710  stoweidlem1  37861  stoweidlem5  37865  stoweidlem7  37867  dirkercncflem1  37965  dirkercncflem4  37968  fourierdlem30  37999  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem48  38018  fourierdlem62  38032  fourierdlem63  38033  fourierdlem68  38038  fourierdlem79  38049  sqwvfoura  38092  etransclem32  38131  hoidmvlelem2  38418  stgoldbwt  38877  evengpop3  38893  evengpoap3  38894  bgoldbtbndlem2  38901  bgoldbtbndlem3  38902  proththdlem  38913  lindslinindimp2lem3  40306  nno  40381  fllogbd  40424  nnolog2flm1  40454
  Copyright terms: Public domain W3C validator