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

Theorem syl6eqbr 4249
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 4222 . 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 1652   class class class wbr 4212
This theorem is referenced by:  syl6eqbrr  4250  domunsn  7257  mapdom1  7272  mapdom2  7278  pm54.43  7887  cdadom1  8066  infmap2  8098  inar1  8650  gruina  8693  xltnegi  10802  leexp1a  11438  discr  11516  facwordi  11580  faclbnd3  11583  hashsnlei  11680  hashgt12el  11682  cnpart  12045  geomulcvg  12653  dvds1  12898  ramz2  13392  ramz  13393  gex1  15225  sylow2a  15253  en1top  17049  en2top  17050  hmph0  17827  ptcmplem2  18084  dscmet  18620  dscopn  18621  xrge0tsms2  18866  htpycc  19005  pcohtpylem  19044  pcopt  19047  pcopt2  19048  pcoass  19049  pcorevlem  19051  vitalilem5  19504  dvef  19864  dveq0  19884  dv11cn  19885  deg1lt0  20014  ply1rem  20086  fta1g  20090  plyremlem  20221  aalioulem3  20251  pige3  20425  relogrn  20459  logneg  20482  cxpaddlelem  20635  mule1  20931  ppiub  20988  dchrabs2  21046  bposlem1  21068  lgseisen  21137  lgsquadlem2  21139  rpvmasumlem  21181  qabvle  21319  ostth3  21332  konigsberg  21709  nmosetn0  22266  nmoo0  22292  siii  22354  bcsiALT  22681  branmfn  23608  ballotlemrc  24788  subfacval3  24875  sconpi1  24926  fz0n  25202  colinearalg  25849  itg2addnclem  26256  ftc1anc  26288  stoweidlem18  27743  stoweidlem55  27780
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator