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

Theorem syl5eqbr 4450
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 2420 . 2  |-  C  =  C
41, 2, 33brtr4g 4449 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418
This theorem is referenced by:  xp1en  7655  map2xp  7739  1sdom  7772  sucxpdom  7778  sniffsupp  7920  wdomima2g  8092  pwsdompw  8623  infunsdom1  8632  infunsdom  8633  infxp  8634  ackbij1lem5  8643  hsmexlem4  8848  imadomg  8951  unidom  8957  unictb  8989  pwcdandom  9081  distrnq  9375  supxrmnf  11592  xov1plusxeqvd  11765  quoremz  12068  quoremnn0ALT  12070  intfrac2  12071  bernneq2  12385  faclbnd4lem1  12464  sqrlem4  13277  reccn2  13627  caucvg  13712  o1fsum  13840  infcvgaux2i  13883  eirrlem  14223  rpnnen2  14245  ruclem12  14260  divalglem5  14342  bitsfzolem  14371  bitsinv1lem  14378  bezoutlem3  14468  lcmsledvdsOLD  14545  lcmfunsnlem  14574  sqnprm  14606  coprmproddvds  14640  prmreclem6  14817  4sqlem6  14839  4sqlem13OLD  14853  4sqlem16OLD  14856  4sqlem17OLD  14857  4sqlem13  14859  4sqlem16  14862  4sqlem17  14863  2expltfac  15015  odcau  17184  sylow3  17213  efginvrel2  17305  lt6abl  17457  ablfac1lem  17629  evlslem2  18663  gzrngunitlem  18960  zringlpirlem3  18982  znfld  19055  chfacffsupp  19804  cpmidpmatlem3  19820  cctop  19945  csdfil  20833  xpsdsval  21320  nrginvrcnlem  21617  icccmplem2  21745  reconnlem2  21749  iscmet3lem3  22146  minveclem2  22254  minveclem4  22260  ivthlem2  22277  ivthlem3  22278  ovolunlem1a  22323  ovolfiniun  22328  ovoliunlem3  22331  ovoliun  22332  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  unmbl  22365  ioombl1lem4  22388  itg2mono  22585  ibladdlem  22651  iblabsr  22661  iblmulc2  22662  dvferm1lem  22810  dvferm2lem  22812  lhop1lem  22839  dvcvx  22846  ftc1a  22863  plyeq0lem  23029  aannenlem3  23148  geolim3  23157  psercnlem1  23242  pserdvlem2  23245  reeff1olem  23263  pilem2  23269  pilem2OLD  23270  pilem3  23271  pilem3OLD  23272  cosq14gt0  23327  cosq14ge0  23328  cosne0  23341  recosf1o  23346  resinf1o  23347  argregt0  23421  logcnlem3  23451  logcnlem4  23452  logf1o2  23457  cxpcn3lem  23549  ang180lem2  23601  acosbnd  23688  atanbndlem  23713  leibpi  23730  cxp2lim  23764  emcllem2  23784  ftalem5  23863  basellem9  23875  vmage0  23908  chpge0  23913  chtub  24000  mersenne  24015  bposlem2  24073  bposlem5  24076  bposlem6  24077  bposlem9  24080  lgseisenlem1  24137  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  chebbnd1lem1  24167  chebbnd1lem2  24168  chebbnd1lem3  24169  mulog2sumlem2  24233  pntpbnd1a  24283  pntibndlem1  24287  pntibndlem3  24290  pntlemc  24293  ostth2  24335  ostth3  24336  smcnlem  26175  minvecolem2  26359  minvecolem4  26364  strlem5  27740  hstrlem5  27748  abrexdomjm  27974  prct  28136  dya2icoseg  28935  omssubadd  28958  omsmeas  28981  oddpwdc  29010  faclim  30166  faclim2  30168  taupilem1  31464  mblfinlem3  31683  mblfinlem4  31684  ibladdnclem  31702  iblmulc2nc  31711  bddiblnc  31716  abrexdom  31761  dalem3  32938  dalem8  32944  dalem25  32972  dalem27  32973  dalem38  32984  dalem44  32990  dalem54  33000  lhpat3  33320  4atexlemunv  33340  4atexlemtlw  33341  4atexlemc  33343  4atexlemnclw  33344  4atexlemex2  33345  4atexlemcnd  33346  cdleme0b  33487  cdleme0c  33488  cdleme0fN  33493  cdlemeulpq  33495  cdleme01N  33496  cdleme0ex1N  33498  cdleme2  33503  cdleme3b  33504  cdleme3c  33505  cdleme3g  33509  cdleme3h  33510  cdleme4a  33514  cdleme7aa  33517  cdleme7c  33520  cdleme7d  33521  cdleme7e  33522  cdleme9  33528  cdleme11fN  33539  cdleme11k  33543  cdleme15d  33552  cdlemednpq  33574  cdleme19c  33581  cdleme20aN  33585  cdleme20e  33589  cdleme21c  33603  cdleme21ct  33605  cdleme22e  33620  cdleme22eALTN  33621  cdleme22f  33622  cdleme23a  33625  cdleme28a  33646  cdleme35f  33730  cdlemeg46frv  33801  cdlemeg46rgv  33804  cdlemeg46req  33805  cdlemg2fv2  33876  cdlemg2m  33880  cdlemg6c  33896  cdlemg31a  33973  cdlemg31b  33974  cdlemk10  34119  cdlemk37  34190  dia2dimlem1  34341  dihjatcclem4  34698  irrapxlem3  35378  pell14qrgapw  35432  dgrsub2  35704  radcnvrat  36304  fmul01  37234  fmul01lt1lem1  37238  fmul01lt1lem2  37239  sumnnodd  37286  stoweidlem1  37434  stoweidlem5  37438  stoweidlem7  37440  dirkercncflem1  37538  dirkercncflem4  37541  fourierdlem30  37572  fourierdlem42  37584  fourierdlem48  37590  fourierdlem62  37604  fourierdlem63  37605  fourierdlem68  37610  fourierdlem79  37621  sqwvfoura  37664  etransclem32  37702  stgoldbwt  38280  evengpop3  38296  evengpoap3  38297  bgoldbtbndlem2  38304  bgoldbtbndlem3  38305  proththdlem  38316  lindslinindimp2lem3  39026  nno  39102  fllogbd  39145  nnolog2flm1  39175
  Copyright terms: Public domain W3C validator