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

Theorem syl5eqbr 4313
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 2433 . 2  |-  C  =  C
41, 2, 33brtr4g 4312 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  xp1en  7385  map2xp  7469  1sdom  7503  sucxpdom  7510  sniffsupp  7647  wdomima2g  7789  pwsdompw  8361  infunsdom1  8370  infunsdom  8371  infxp  8372  ackbij1lem5  8381  hsmexlem4  8586  imadomg  8689  unidom  8695  unictb  8727  pwcdandom  8822  distrnq  9118  supxrmnf  11268  xov1plusxeqvd  11418  quoremz  11678  quoremnn0ALT  11680  intfrac2  11681  bernneq2  11975  faclbnd4lem1  12053  sqrlem4  12719  reccn2  13058  caucvg  13140  o1fsum  13259  infcvgaux2i  13303  eirrlem  13469  rpnnen2  13491  ruclem12  13506  divalglem5  13584  bitsfzolem  13613  bitsinv1lem  13620  bezoutlem3  13707  sqnprm  13767  prmreclem6  13965  4sqlem6  13987  4sqlem13  14001  4sqlem16  14004  4sqlem17  14005  2expltfac  14102  odcau  16083  sylow3  16112  efginvrel2  16204  lt6abl  16351  ablfac1lem  16543  evlslem2  17525  gzrngunitlem  17721  zringlpirlem3  17747  zlpirlem3  17752  znfld  17835  cctop  18452  csdfil  19309  xpsdsval  19798  nrginvrcnlem  20113  icccmplem2  20242  reconnlem2  20246  iscmet3lem3  20643  minveclem2  20755  minveclem4  20761  ivthlem2  20778  ivthlem3  20779  ovolunlem1a  20821  ovolfiniun  20826  ovoliunlem3  20829  ovoliun  20830  ovolicc2lem4  20845  unmbl  20861  ioombl1lem4  20884  itg2mono  21073  ibladdlem  21139  iblabsr  21149  iblmulc2  21150  dvferm1lem  21298  dvferm2lem  21300  lhop1lem  21327  dvcvx  21334  ftc1a  21351  plyeq0lem  21563  aannenlem3  21681  geolim3  21690  psercnlem1  21775  pserdvlem2  21778  reeff1olem  21796  pilem2  21802  pilem3  21803  cosq14gt0  21857  cosq14ge0  21858  cosne0  21871  recosf1o  21876  resinf1o  21877  argregt0  21944  logcnlem3  21974  logcnlem4  21975  logf1o2  21980  cxpcn3lem  22070  ang180lem2  22091  acosbnd  22180  atanbndlem  22205  leibpi  22222  cxp2lim  22255  emcllem2  22275  ftalem5  22299  basellem9  22311  vmage0  22344  chpge0  22349  chtub  22436  mersenne  22451  bposlem2  22509  bposlem5  22512  bposlem6  22513  bposlem9  22516  lgseisenlem1  22573  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  chebbnd1lem1  22603  chebbnd1lem2  22604  chebbnd1lem3  22605  mulog2sumlem2  22669  pntpbnd1a  22719  pntibndlem1  22723  pntibndlem3  22726  pntlemc  22729  ostth2  22771  ostth3  22772  smcnlem  23915  minvecolem2  24099  minvecolem4  24104  strlem5  25482  hstrlem5  25490  abrexdomjm  25712  prct  25836  dya2icoseg  26546  oddpwdc  26585  faclim  27399  faclim2  27401  mblfinlem3  28274  mblfinlem4  28275  ibladdnclem  28292  iblmulc2nc  28301  bddiblnc  28306  abrexdom  28468  irrapxlem3  29010  pell14qrgapw  29062  dgrsub2  29336  fmul01  29606  fmul01lt1lem1  29610  fmul01lt1lem2  29611  stoweidlem1  29642  stoweidlem5  29646  stoweidlem7  29648  lindslinindimp2lem3  30724  dalem3  32902  dalem8  32908  dalem25  32936  dalem27  32937  dalem38  32948  dalem44  32954  dalem54  32964  lhpat3  33284  4atexlemunv  33304  4atexlemtlw  33305  4atexlemc  33307  4atexlemnclw  33308  4atexlemex2  33309  4atexlemcnd  33310  cdleme0b  33450  cdleme0c  33451  cdleme0fN  33456  cdlemeulpq  33458  cdleme01N  33459  cdleme0ex1N  33461  cdleme2  33466  cdleme3b  33467  cdleme3c  33468  cdleme3g  33472  cdleme3h  33473  cdleme4a  33477  cdleme7aa  33480  cdleme7c  33483  cdleme7d  33484  cdleme7e  33485  cdleme9  33491  cdleme11fN  33502  cdleme11k  33506  cdleme15d  33515  cdlemednpq  33537  cdleme19c  33543  cdleme20aN  33547  cdleme20e  33551  cdleme21c  33565  cdleme21ct  33567  cdleme22e  33582  cdleme22eALTN  33583  cdleme22f  33584  cdleme23a  33587  cdleme28a  33608  cdleme35f  33692  cdlemeg46frv  33763  cdlemeg46rgv  33766  cdlemeg46req  33767  cdlemg2fv2  33838  cdlemg2m  33842  cdlemg6c  33858  cdlemg31a  33935  cdlemg31b  33936  cdlemk10  34081  cdlemk37  34152  dia2dimlem1  34303  dihjatcclem4  34660  taupilem1  35209
  Copyright terms: Public domain W3C validator