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

Theorem syl6eqbr 4324
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 4297 . 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 1369   class class class wbr 4287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288
This theorem is referenced by:  syl6eqbrr  4325  domunsn  7453  mapdom1  7468  mapdom2  7474  pm54.43  8162  cdadom1  8347  infmap2  8379  inar1  8934  gruina  8977  xltnegi  11178  leexp1a  11914  discr  11993  facwordi  12057  faclbnd3  12060  hashsnlei  12162  hashgt12el  12165  cnpart  12721  geomulcvg  13328  dvds1  13573  ramz2  14077  ramz  14078  gex1  16081  sylow2a  16109  en1top  18569  en2top  18570  hmph0  19348  ptcmplem2  19605  dscmet  20145  dscopn  20146  xrge0tsms2  20392  htpycc  20532  pcohtpylem  20571  pcopt  20574  pcopt2  20575  pcoass  20576  pcorevlem  20578  vitalilem5  21072  dvef  21432  dveq0  21452  dv11cn  21453  deg1lt0  21542  ply1rem  21615  fta1g  21619  plyremlem  21750  aalioulem3  21780  pige3  21959  relogrn  21993  logneg  22016  cxpaddlelem  22169  mule1  22466  ppiub  22523  dchrabs2  22581  bposlem1  22603  lgseisen  22672  lgsquadlem2  22674  rpvmasumlem  22716  qabvle  22854  ostth3  22867  colinearalg  23124  eengstr  23194  konigsberg  23576  nmosetn0  24133  nmoo0  24159  siii  24221  bcsiALT  24549  branmfn  25477  ballotlemrc  26882  subfacval3  27046  sconpi1  27097  fz0n  27358  itg2addnclem  28414  ftc1anc  28446  stoweidlem18  29784  stoweidlem55  29821  exple2lt6  30736
  Copyright terms: Public domain W3C validator