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

Theorem syl5eqbr 4320
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 2438 . 2  |-  C  =  C
41, 2, 33brtr4g 4319 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  xp1en  7389  map2xp  7473  1sdom  7507  sucxpdom  7514  sniffsupp  7651  wdomima2g  7793  pwsdompw  8365  infunsdom1  8374  infunsdom  8375  infxp  8376  ackbij1lem5  8385  hsmexlem4  8590  imadomg  8693  unidom  8699  unictb  8731  pwcdandom  8826  distrnq  9122  supxrmnf  11272  xov1plusxeqvd  11423  quoremz  11686  quoremnn0ALT  11688  intfrac2  11689  bernneq2  11983  faclbnd4lem1  12061  sqrlem4  12727  reccn2  13066  caucvg  13148  o1fsum  13268  infcvgaux2i  13312  eirrlem  13478  rpnnen2  13500  ruclem12  13515  divalglem5  13593  bitsfzolem  13622  bitsinv1lem  13629  bezoutlem3  13716  sqnprm  13776  prmreclem6  13974  4sqlem6  13996  4sqlem13  14010  4sqlem16  14013  4sqlem17  14014  2expltfac  14111  odcau  16094  sylow3  16123  efginvrel2  16215  lt6abl  16362  ablfac1lem  16557  evlslem2  17572  gzrngunitlem  17852  zringlpirlem3  17880  zlpirlem3  17885  znfld  17968  cctop  18585  csdfil  19442  xpsdsval  19931  nrginvrcnlem  20246  icccmplem2  20375  reconnlem2  20379  iscmet3lem3  20776  minveclem2  20888  minveclem4  20894  ivthlem2  20911  ivthlem3  20912  ovolunlem1a  20954  ovolfiniun  20959  ovoliunlem3  20962  ovoliun  20963  ovolicc2lem4  20978  unmbl  20994  ioombl1lem4  21017  itg2mono  21206  ibladdlem  21272  iblabsr  21282  iblmulc2  21283  dvferm1lem  21431  dvferm2lem  21433  lhop1lem  21460  dvcvx  21467  ftc1a  21484  plyeq0lem  21653  aannenlem3  21771  geolim3  21780  psercnlem1  21865  pserdvlem2  21868  reeff1olem  21886  pilem2  21892  pilem3  21893  cosq14gt0  21947  cosq14ge0  21948  cosne0  21961  recosf1o  21966  resinf1o  21967  argregt0  22034  logcnlem3  22064  logcnlem4  22065  logf1o2  22070  cxpcn3lem  22160  ang180lem2  22181  acosbnd  22270  atanbndlem  22295  leibpi  22312  cxp2lim  22345  emcllem2  22365  ftalem5  22389  basellem9  22401  vmage0  22434  chpge0  22439  chtub  22526  mersenne  22541  bposlem2  22599  bposlem5  22602  bposlem6  22603  bposlem9  22606  lgseisenlem1  22663  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  mulog2sumlem2  22759  pntpbnd1a  22809  pntibndlem1  22813  pntibndlem3  22816  pntlemc  22819  ostth2  22861  ostth3  22862  smcnlem  24043  minvecolem2  24227  minvecolem4  24232  strlem5  25610  hstrlem5  25618  abrexdomjm  25839  prct  25963  dya2icoseg  26644  oddpwdc  26689  faclim  27503  faclim2  27505  mblfinlem3  28383  mblfinlem4  28384  ibladdnclem  28401  iblmulc2nc  28410  bddiblnc  28415  abrexdom  28577  irrapxlem3  29118  pell14qrgapw  29170  dgrsub2  29444  fmul01  29714  fmul01lt1lem1  29718  fmul01lt1lem2  29719  stoweidlem1  29749  stoweidlem5  29753  stoweidlem7  29755  lindslinindimp2lem3  30883  dalem3  33148  dalem8  33154  dalem25  33182  dalem27  33183  dalem38  33194  dalem44  33200  dalem54  33210  lhpat3  33530  4atexlemunv  33550  4atexlemtlw  33551  4atexlemc  33553  4atexlemnclw  33554  4atexlemex2  33555  4atexlemcnd  33556  cdleme0b  33696  cdleme0c  33697  cdleme0fN  33702  cdlemeulpq  33704  cdleme01N  33705  cdleme0ex1N  33707  cdleme2  33712  cdleme3b  33713  cdleme3c  33714  cdleme3g  33718  cdleme3h  33719  cdleme4a  33723  cdleme7aa  33726  cdleme7c  33729  cdleme7d  33730  cdleme7e  33731  cdleme9  33737  cdleme11fN  33748  cdleme11k  33752  cdleme15d  33761  cdlemednpq  33783  cdleme19c  33789  cdleme20aN  33793  cdleme20e  33797  cdleme21c  33811  cdleme21ct  33813  cdleme22e  33828  cdleme22eALTN  33829  cdleme22f  33830  cdleme23a  33833  cdleme28a  33854  cdleme35f  33938  cdlemeg46frv  34009  cdlemeg46rgv  34012  cdlemeg46req  34013  cdlemg2fv2  34084  cdlemg2m  34088  cdlemg6c  34104  cdlemg31a  34181  cdlemg31b  34182  cdlemk10  34327  cdlemk37  34398  dia2dimlem1  34549  dihjatcclem4  34906  taupilem1  35455
  Copyright terms: Public domain W3C validator