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

Theorem syl5eqbr 4466
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 2441 . 2  |-  C  =  C
41, 2, 33brtr4g 4465 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381   class class class wbr 4433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434
This theorem is referenced by:  xp1en  7601  map2xp  7685  1sdom  7720  sucxpdom  7727  sniffsupp  7867  wdomima2g  8010  pwsdompw  8582  infunsdom1  8591  infunsdom  8592  infxp  8593  ackbij1lem5  8602  hsmexlem4  8807  imadomg  8910  unidom  8916  unictb  8948  pwcdandom  9043  distrnq  9337  supxrmnf  11513  xov1plusxeqvd  11670  quoremz  11956  quoremnn0ALT  11958  intfrac2  11959  bernneq2  12267  faclbnd4lem1  12345  sqrlem4  13053  reccn2  13393  caucvg  13475  o1fsum  13601  infcvgaux2i  13643  eirrlem  13809  rpnnen2  13831  ruclem12  13846  divalglem5  13927  bitsfzolem  13956  bitsinv1lem  13963  bezoutlem3  14050  sqnprm  14111  prmreclem6  14311  4sqlem6  14333  4sqlem13  14347  4sqlem16  14350  4sqlem17  14351  2expltfac  14449  odcau  16493  sylow3  16522  efginvrel2  16614  lt6abl  16766  ablfac1lem  16987  evlslem2  18048  gzrngunitlem  18350  zringlpirlem3  18378  zlpirlem3  18383  znfld  18466  chfacffsupp  19224  cpmidpmatlem3  19240  cctop  19373  csdfil  20261  xpsdsval  20750  nrginvrcnlem  21065  icccmplem2  21194  reconnlem2  21198  iscmet3lem3  21595  minveclem2  21707  minveclem4  21713  ivthlem2  21730  ivthlem3  21731  ovolunlem1a  21773  ovolfiniun  21778  ovoliunlem3  21781  ovoliun  21782  ovolicc2lem4  21797  unmbl  21814  ioombl1lem4  21837  itg2mono  22026  ibladdlem  22092  iblabsr  22102  iblmulc2  22103  dvferm1lem  22251  dvferm2lem  22253  lhop1lem  22280  dvcvx  22287  ftc1a  22304  plyeq0lem  22473  aannenlem3  22591  geolim3  22600  psercnlem1  22685  pserdvlem2  22688  reeff1olem  22706  pilem2  22712  pilem3  22713  cosq14gt0  22768  cosq14ge0  22769  cosne0  22782  recosf1o  22787  resinf1o  22788  argregt0  22860  logcnlem3  22890  logcnlem4  22891  logf1o2  22896  cxpcn3lem  22986  ang180lem2  23007  acosbnd  23096  atanbndlem  23121  leibpi  23138  cxp2lim  23171  emcllem2  23191  ftalem5  23215  basellem9  23227  vmage0  23260  chpge0  23265  chtub  23352  mersenne  23367  bposlem2  23425  bposlem5  23428  bposlem6  23429  bposlem9  23432  lgseisenlem1  23489  lgsquadlem1  23494  lgsquadlem2  23495  lgsquadlem3  23496  chebbnd1lem1  23519  chebbnd1lem2  23520  chebbnd1lem3  23521  mulog2sumlem2  23585  pntpbnd1a  23635  pntibndlem1  23639  pntibndlem3  23642  pntlemc  23645  ostth2  23687  ostth3  23688  smcnlem  25472  minvecolem2  25656  minvecolem4  25661  strlem5  27039  hstrlem5  27047  abrexdomjm  27270  prct  27400  dya2icoseg  28114  oddpwdc  28159  faclim  29139  faclim2  29141  mblfinlem3  30021  mblfinlem4  30022  ibladdnclem  30039  iblmulc2nc  30048  bddiblnc  30053  abrexdom  30189  irrapxlem3  30728  pell14qrgapw  30780  dgrsub2  31052  radcnvrat  31164  fmul01  31498  fmul01lt1lem1  31502  fmul01lt1lem2  31503  sumnnodd  31540  stoweidlem1  31668  stoweidlem5  31672  stoweidlem7  31674  dirkercncflem1  31770  dirkercncflem4  31773  fourierdlem30  31804  fourierdlem42  31816  fourierdlem48  31822  fourierdlem62  31836  fourierdlem63  31837  fourierdlem68  31842  fourierdlem79  31853  sqwvfoura  31896  lindslinindimp2lem3  32771  dalem3  35090  dalem8  35096  dalem25  35124  dalem27  35125  dalem38  35136  dalem44  35142  dalem54  35152  lhpat3  35472  4atexlemunv  35492  4atexlemtlw  35493  4atexlemc  35495  4atexlemnclw  35496  4atexlemex2  35497  4atexlemcnd  35498  cdleme0b  35639  cdleme0c  35640  cdleme0fN  35645  cdlemeulpq  35647  cdleme01N  35648  cdleme0ex1N  35650  cdleme2  35655  cdleme3b  35656  cdleme3c  35657  cdleme3g  35661  cdleme3h  35662  cdleme4a  35666  cdleme7aa  35669  cdleme7c  35672  cdleme7d  35673  cdleme7e  35674  cdleme9  35680  cdleme11fN  35691  cdleme11k  35695  cdleme15d  35704  cdlemednpq  35726  cdleme19c  35733  cdleme20aN  35737  cdleme20e  35741  cdleme21c  35755  cdleme21ct  35757  cdleme22e  35772  cdleme22eALTN  35773  cdleme22f  35774  cdleme23a  35777  cdleme28a  35798  cdleme35f  35882  cdlemeg46frv  35953  cdlemeg46rgv  35956  cdlemeg46req  35957  cdlemg2fv2  36028  cdlemg2m  36032  cdlemg6c  36048  cdlemg31a  36125  cdlemg31b  36126  cdlemk10  36271  cdlemk37  36342  dia2dimlem1  36493  dihjatcclem4  36850  taupilem1  37398
  Copyright terms: Public domain W3C validator