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

Theorem syl5eqbr 4472
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 2454 . 2  |-  C  =  C
41, 2, 33brtr4g 4471 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398   class class class wbr 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440
This theorem is referenced by:  xp1en  7596  map2xp  7680  1sdom  7715  sucxpdom  7722  sniffsupp  7861  wdomima2g  8004  pwsdompw  8575  infunsdom1  8584  infunsdom  8585  infxp  8586  ackbij1lem5  8595  hsmexlem4  8800  imadomg  8903  unidom  8909  unictb  8941  pwcdandom  9034  distrnq  9328  supxrmnf  11512  xov1plusxeqvd  11669  quoremz  11964  quoremnn0ALT  11966  intfrac2  11967  bernneq2  12275  faclbnd4lem1  12353  sqrlem4  13161  reccn2  13501  caucvg  13583  o1fsum  13709  infcvgaux2i  13751  eirrlem  14019  rpnnen2  14043  ruclem12  14058  divalglem5  14139  bitsfzolem  14168  bitsinv1lem  14175  bezoutlem3  14262  sqnprm  14323  prmreclem6  14523  4sqlem6  14545  4sqlem13  14559  4sqlem16  14562  4sqlem17  14563  2expltfac  14661  odcau  16823  sylow3  16852  efginvrel2  16944  lt6abl  17096  ablfac1lem  17314  evlslem2  18375  gzrngunitlem  18677  zringlpirlem3  18699  znfld  18772  chfacffsupp  19524  cpmidpmatlem3  19540  cctop  19674  csdfil  20561  xpsdsval  21050  nrginvrcnlem  21365  icccmplem2  21494  reconnlem2  21498  iscmet3lem3  21895  minveclem2  22007  minveclem4  22013  ivthlem2  22030  ivthlem3  22031  ovolunlem1a  22073  ovolfiniun  22078  ovoliunlem3  22081  ovoliun  22082  ovolicc2lem4  22097  unmbl  22114  ioombl1lem4  22137  itg2mono  22326  ibladdlem  22392  iblabsr  22402  iblmulc2  22403  dvferm1lem  22551  dvferm2lem  22553  lhop1lem  22580  dvcvx  22587  ftc1a  22604  plyeq0lem  22773  aannenlem3  22892  geolim3  22901  psercnlem1  22986  pserdvlem2  22989  reeff1olem  23007  pilem2  23013  pilem3  23014  cosq14gt0  23069  cosq14ge0  23070  cosne0  23083  recosf1o  23088  resinf1o  23089  argregt0  23163  logcnlem3  23193  logcnlem4  23194  logf1o2  23199  cxpcn3lem  23289  ang180lem2  23341  acosbnd  23428  atanbndlem  23453  leibpi  23470  cxp2lim  23504  emcllem2  23524  ftalem5  23548  basellem9  23560  vmage0  23593  chpge0  23598  chtub  23685  mersenne  23700  bposlem2  23758  bposlem5  23761  bposlem6  23762  bposlem9  23765  lgseisenlem1  23822  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  chebbnd1lem1  23852  chebbnd1lem2  23853  chebbnd1lem3  23854  mulog2sumlem2  23918  pntpbnd1a  23968  pntibndlem1  23972  pntibndlem3  23975  pntlemc  23978  ostth2  24020  ostth3  24021  smcnlem  25805  minvecolem2  25989  minvecolem4  25994  strlem5  27372  hstrlem5  27380  abrexdomjm  27604  prct  27765  dya2icoseg  28485  omssubadd  28508  omsmeas  28531  oddpwdc  28557  faclim  29412  faclim2  29414  mblfinlem3  30293  mblfinlem4  30294  ibladdnclem  30311  iblmulc2nc  30320  bddiblnc  30325  abrexdom  30461  irrapxlem3  30999  pell14qrgapw  31051  dgrsub2  31325  radcnvrat  31436  fmul01  31813  fmul01lt1lem1  31817  fmul01lt1lem2  31818  sumnnodd  31875  stoweidlem1  32022  stoweidlem5  32026  stoweidlem7  32028  dirkercncflem1  32124  dirkercncflem4  32127  fourierdlem30  32158  fourierdlem42  32170  fourierdlem48  32176  fourierdlem62  32190  fourierdlem63  32191  fourierdlem68  32196  fourierdlem79  32207  sqwvfoura  32250  etransclem32  32288  lindslinindimp2lem3  33315  nno  33392  fllogbd  33435  nnolog2flm1  33465  dalem3  35785  dalem8  35791  dalem25  35819  dalem27  35820  dalem38  35831  dalem44  35837  dalem54  35847  lhpat3  36167  4atexlemunv  36187  4atexlemtlw  36188  4atexlemc  36190  4atexlemnclw  36191  4atexlemex2  36192  4atexlemcnd  36193  cdleme0b  36334  cdleme0c  36335  cdleme0fN  36340  cdlemeulpq  36342  cdleme01N  36343  cdleme0ex1N  36345  cdleme2  36350  cdleme3b  36351  cdleme3c  36352  cdleme3g  36356  cdleme3h  36357  cdleme4a  36361  cdleme7aa  36364  cdleme7c  36367  cdleme7d  36368  cdleme7e  36369  cdleme9  36375  cdleme11fN  36386  cdleme11k  36390  cdleme15d  36399  cdlemednpq  36421  cdleme19c  36428  cdleme20aN  36432  cdleme20e  36436  cdleme21c  36450  cdleme21ct  36452  cdleme22e  36467  cdleme22eALTN  36468  cdleme22f  36469  cdleme23a  36472  cdleme28a  36493  cdleme35f  36577  cdlemeg46frv  36648  cdlemeg46rgv  36651  cdlemeg46req  36652  cdlemg2fv2  36723  cdlemg2m  36727  cdlemg6c  36743  cdlemg31a  36820  cdlemg31b  36821  cdlemk10  36966  cdlemk37  37037  dia2dimlem1  37188  dihjatcclem4  37545  taupilem1  38093
  Copyright terms: Public domain W3C validator