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

Theorem syl5eqbr 4237
Description: B 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 2435 . 2  |-  C  =  C
41, 2, 33brtr4g 4236 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4204
This theorem is referenced by:  xp1en  7186  map2xp  7269  1sdom  7303  sucxpdom  7310  wdomima2g  7546  pwsdompw  8076  infunsdom1  8085  infunsdom  8086  infxp  8087  ackbij1lem5  8096  hsmexlem4  8301  imadomg  8404  unidom  8410  unictb  8442  pwcdandom  8534  distrnq  8830  supxrmnf  10888  xov1plusxeqvd  11033  quoremz  11228  quoremnn0ALT  11230  intfrac2  11231  bernneq2  11498  faclbnd4lem1  11576  sqrlem4  12043  reccn2  12382  caucvg  12464  o1fsum  12584  infcvgaux2i  12629  eirrlem  12795  rpnnen2  12817  ruclem12  12832  divalglem5  12909  bitsfzolem  12938  bitsinv1lem  12945  bezoutlem3  13032  sqnprm  13090  prmreclem6  13281  4sqlem6  13303  4sqlem13  13317  4sqlem16  13320  4sqlem17  13321  2expltfac  13418  odcau  15230  sylow3  15259  efginvrel2  15351  lt6abl  15496  ablfac1lem  15618  gzrngunitlem  16755  zlpirlem3  16762  znfld  16833  cctop  17062  csdfil  17918  xpsdsval  18403  nrginvrcnlem  18718  icccmplem2  18846  reconnlem2  18850  iscmet3lem3  19235  minveclem2  19319  minveclem4  19325  ivthlem2  19341  ivthlem3  19342  ovolunlem1a  19384  ovolfiniun  19389  ovoliunlem3  19392  ovoliun  19393  ovolicc2lem4  19408  unmbl  19424  ioombl1lem4  19447  itg2mono  19637  ibladdlem  19703  iblabsr  19713  iblmulc2  19714  dvferm1lem  19860  dvferm2lem  19862  lhop1lem  19889  dvcvx  19896  ftc1a  19913  plyeq0lem  20121  aannenlem3  20239  geolim3  20248  psercnlem1  20333  pserdvlem2  20336  reeff1olem  20354  pilem2  20360  pilem3  20361  cosq14gt0  20410  cosq14ge0  20411  cosne0  20424  recosf1o  20429  resinf1o  20430  argregt0  20497  logcnlem3  20527  logcnlem4  20528  logf1o2  20533  cxpcn3lem  20623  ang180lem2  20644  acosbnd  20732  atanbndlem  20757  leibpi  20774  cxp2lim  20807  emcllem2  20827  ftalem5  20851  basellem9  20863  vmage0  20896  chpge0  20901  chtub  20988  mersenne  21003  bposlem2  21061  bposlem5  21064  bposlem6  21065  bposlem9  21068  lgseisenlem1  21125  lgsquadlem1  21130  lgsquadlem2  21131  lgsquadlem3  21132  chebbnd1lem1  21155  chebbnd1lem2  21156  chebbnd1lem3  21157  mulog2sumlem2  21221  pntpbnd1a  21271  pntibndlem1  21275  pntibndlem3  21278  pntlemc  21281  ostth2  21323  ostth3  21324  smcnlem  22185  minvecolem2  22369  minvecolem4  22374  strlem5  23750  hstrlem5  23758  abrexdomjm  23980  prct  24096  dya2icoseg  24619  faclim  25357  faclim2  25359  mblfinlem2  26235  mblfinlem3  26236  ibladdnclem  26251  iblmulc2nc  26260  bddiblnc  26265  abrexdom  26423  irrapxlem3  26878  pell14qrgapw  26930  dgrsub2  27307  fmul01  27677  fmul01lt1lem1  27681  fmul01lt1lem2  27682  stoweidlem1  27717  stoweidlem5  27721  stoweidlem7  27723  dalem3  30398  dalem8  30404  dalem25  30432  dalem27  30433  dalem38  30444  dalem44  30450  dalem54  30460  lhpat3  30780  4atexlemunv  30800  4atexlemtlw  30801  4atexlemc  30803  4atexlemnclw  30804  4atexlemex2  30805  4atexlemcnd  30806  cdleme0b  30946  cdleme0c  30947  cdleme0fN  30952  cdlemeulpq  30954  cdleme01N  30955  cdleme0ex1N  30957  cdleme2  30962  cdleme3b  30963  cdleme3c  30964  cdleme3g  30968  cdleme3h  30969  cdleme4a  30973  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme9  30987  cdleme11fN  30998  cdleme11k  31002  cdleme15d  31011  cdlemednpq  31033  cdleme19c  31039  cdleme20aN  31043  cdleme20e  31047  cdleme21c  31061  cdleme21ct  31063  cdleme22e  31078  cdleme22eALTN  31079  cdleme22f  31080  cdleme23a  31083  cdleme28a  31104  cdleme35f  31188  cdlemeg46frv  31259  cdlemeg46rgv  31262  cdlemeg46req  31263  cdlemg2fv2  31334  cdlemg2m  31338  cdlemg6c  31354  cdlemg31a  31431  cdlemg31b  31432  cdlemk10  31577  cdlemk37  31648  dia2dimlem1  31799  dihjatcclem4  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator