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

Theorem syl6eqbr 4060
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 4033 . 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 1623   class class class wbr 4023
This theorem is referenced by:  syl6eqbrr  4061  domunsn  7011  mapdom1  7026  mapdom2  7032  pm54.43  7633  cdadom1  7812  infmap2  7844  inar1  8397  gruina  8440  xltnegi  10543  leexp1a  11160  discr  11238  facwordi  11302  faclbnd3  11305  hashsnlei  11376  cnpart  11725  geomulcvg  12332  dvds1  12577  ramz2  13071  ramz  13072  gex1  14902  sylow2a  14930  en1top  16722  en2top  16723  hmph0  17486  ptcmplem2  17747  dscmet  18095  dscopn  18096  xrge0tsms2  18340  htpycc  18478  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  vitalilem5  18967  dvef  19327  dveq0  19347  dv11cn  19348  deg1lt0  19477  ply1rem  19549  fta1g  19553  plyremlem  19684  aalioulem3  19714  pige3  19885  relogrn  19919  logneg  19941  cxpaddlelem  20091  mule1  20386  ppiub  20443  dchrabs2  20501  bposlem1  20523  lgseisen  20592  lgsquadlem2  20594  rpvmasumlem  20636  qabvle  20774  ostth3  20787  nmosetn0  21343  nmoo0  21369  siii  21431  bcsiALT  21758  branmfn  22685  ballotlemrc  23089  subfacval3  23720  sconpi1  23770  konigsberg  23911  fz0n  24097  colinearalg  24538  cntrset  25602  stoweidlem18  27767
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator