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

Theorem syl6eqbr 4484
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 4457 . 2  |-  ( ph  ->  ( A R C  <-> 
B R C ) )
41, 3mpbiri 233 1  |-  ( ph  ->  A R C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   class class class wbr 4447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448
This theorem is referenced by:  syl6eqbrr  4485  domunsn  7664  mapdom1  7679  mapdom2  7685  pm54.43  8377  cdadom1  8562  infmap2  8594  inar1  9149  gruina  9192  xltnegi  11411  leexp1a  12188  discr  12267  facwordi  12331  faclbnd3  12334  hashsnlei  12439  hashgt12el  12442  cnpart  13032  geomulcvg  13644  dvds1  13889  ramz2  14397  ramz  14398  gex1  16407  sylow2a  16435  en1top  19252  en2top  19253  hmph0  20031  ptcmplem2  20288  dscmet  20828  dscopn  20829  xrge0tsms2  21075  htpycc  21215  pcohtpylem  21254  pcopt  21257  pcopt2  21258  pcoass  21259  pcorevlem  21261  vitalilem5  21756  dvef  22116  dveq0  22136  dv11cn  22137  deg1lt0  22226  ply1rem  22299  fta1g  22303  plyremlem  22434  aalioulem3  22464  pige3  22643  relogrn  22677  logneg  22700  cxpaddlelem  22853  mule1  23150  ppiub  23207  dchrabs2  23265  bposlem1  23287  lgseisen  23356  lgsquadlem2  23358  rpvmasumlem  23400  qabvle  23538  ostth3  23551  colinearalg  23889  eengstr  23959  konigsberg  24663  nmosetn0  25356  nmoo0  25382  siii  25444  bcsiALT  25772  branmfn  26700  ballotlemrc  28109  subfacval3  28273  sconpi1  28324  fz0n  28585  itg2addnclem  29643  ftc1anc  29675  stoweidlem18  31318  stoweidlem55  31355  fourierdlem62  31469  fourierswlem  31531  exple2lt6  32022
  Copyright terms: Public domain W3C validator