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

Theorem syl6eqbr 4209
Description: A chained equality inference for a binary relation. (Contributed by NM, 12-Oct-1999.)
Hypotheses
Ref Expression
syl6eqbr.1  |-  ( ph  ->  A  =  B )
syl6eqbr.2  |-  B R C
Assertion
Ref Expression
syl6eqbr  |-  ( ph  ->  A R C )

Proof of Theorem syl6eqbr
StepHypRef Expression
1 syl6eqbr.2 . 2  |-  B R C
2 syl6eqbr.1 . . 3  |-  ( ph  ->  A  =  B )
32breq1d 4182 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbiri 225 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   class class class wbr 4172
This theorem is referenced by:  syl6eqbrr  4210  domunsn  7216  mapdom1  7231  mapdom2  7237  pm54.43  7843  cdadom1  8022  infmap2  8054  inar1  8606  gruina  8649  xltnegi  10758  leexp1a  11393  discr  11471  facwordi  11535  faclbnd3  11538  hashsnlei  11635  hashgt12el  11637  cnpart  12000  geomulcvg  12608  dvds1  12853  ramz2  13347  ramz  13348  gex1  15180  sylow2a  15208  en1top  17004  en2top  17005  hmph0  17780  ptcmplem2  18037  dscmet  18573  dscopn  18574  xrge0tsms2  18819  htpycc  18958  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  vitalilem5  19457  dvef  19817  dveq0  19837  dv11cn  19838  deg1lt0  19967  ply1rem  20039  fta1g  20043  plyremlem  20174  aalioulem3  20204  pige3  20378  relogrn  20412  logneg  20435  cxpaddlelem  20588  mule1  20884  ppiub  20941  dchrabs2  20999  bposlem1  21021  lgseisen  21090  lgsquadlem2  21092  rpvmasumlem  21134  qabvle  21272  ostth3  21285  konigsberg  21662  nmosetn0  22219  nmoo0  22245  siii  22307  bcsiALT  22634  branmfn  23561  ballotlemrc  24741  subfacval3  24828  sconpi1  24879  fz0n  25155  colinearalg  25753  itg2addnclem  26155  stoweidlem18  27634  stoweidlem55  27671
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator