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

Theorem syl6eqbr 4436
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 4409 . 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 1370   class class class wbr 4399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400
This theorem is referenced by:  syl6eqbrr  4437  domunsn  7570  mapdom1  7585  mapdom2  7591  pm54.43  8280  cdadom1  8465  infmap2  8497  inar1  9052  gruina  9095  xltnegi  11296  leexp1a  12038  discr  12117  facwordi  12181  faclbnd3  12184  hashsnlei  12287  hashgt12el  12290  cnpart  12846  geomulcvg  13453  dvds1  13698  ramz2  14202  ramz  14203  gex1  16210  sylow2a  16238  en1top  18720  en2top  18721  hmph0  19499  ptcmplem2  19756  dscmet  20296  dscopn  20297  xrge0tsms2  20543  htpycc  20683  pcohtpylem  20722  pcopt  20725  pcopt2  20726  pcoass  20727  pcorevlem  20729  vitalilem5  21224  dvef  21584  dveq0  21604  dv11cn  21605  deg1lt0  21694  ply1rem  21767  fta1g  21771  plyremlem  21902  aalioulem3  21932  pige3  22111  relogrn  22145  logneg  22168  cxpaddlelem  22321  mule1  22618  ppiub  22675  dchrabs2  22733  bposlem1  22755  lgseisen  22824  lgsquadlem2  22826  rpvmasumlem  22868  qabvle  23006  ostth3  23019  colinearalg  23307  eengstr  23377  konigsberg  23759  nmosetn0  24316  nmoo0  24342  siii  24404  bcsiALT  24732  branmfn  25660  ballotlemrc  27056  subfacval3  27220  sconpi1  27271  fz0n  27532  itg2addnclem  28590  ftc1anc  28622  stoweidlem18  29960  stoweidlem55  29997  exple2lt6  30916
  Copyright terms: Public domain W3C validator