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

Theorem syl6eqbr 4076
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 4049 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbiri 224 1  |-  ( ph  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  syl6eqbrr  4077  domunsn  7027  mapdom1  7042  mapdom2  7048  pm54.43  7649  cdadom1  7828  infmap2  7860  inar1  8413  gruina  8456  xltnegi  10559  leexp1a  11176  discr  11254  facwordi  11318  faclbnd3  11321  hashsnlei  11392  cnpart  11741  geomulcvg  12348  dvds1  12593  ramz2  13087  ramz  13088  gex1  14918  sylow2a  14946  en1top  16738  en2top  16739  hmph0  17502  ptcmplem2  17763  dscmet  18111  dscopn  18112  xrge0tsms2  18356  htpycc  18494  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  vitalilem5  18983  dvef  19343  dveq0  19363  dv11cn  19364  deg1lt0  19493  ply1rem  19565  fta1g  19569  plyremlem  19700  aalioulem3  19730  pige3  19901  relogrn  19935  logneg  19957  cxpaddlelem  20107  mule1  20402  ppiub  20459  dchrabs2  20517  bposlem1  20539  lgseisen  20608  lgsquadlem2  20610  rpvmasumlem  20652  qabvle  20790  ostth3  20803  nmosetn0  21359  nmoo0  21385  siii  21447  bcsiALT  21774  branmfn  22701  ballotlemrc  23105  subfacval3  23735  sconpi1  23785  konigsberg  23926  fz0n  24112  colinearalg  24610  itg2addnclem  25003  cntrset  25705  stoweidlem18  27870  hashgt12el  28218
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator