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

Theorem syl6eqbr 4431
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 4404 . 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 1405   class class class wbr 4394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395
This theorem is referenced by:  syl6eqbrr  4432  domunsn  7704  mapdom1  7719  mapdom2  7725  pm54.43  8412  cdadom1  8597  infmap2  8629  inar1  9182  gruina  9225  xltnegi  11467  leexp1a  12267  discr  12345  facwordi  12409  faclbnd3  12412  hashsnlei  12525  hashgt12el  12528  cnpart  13220  geomulcvg  13835  dvds1  14241  ramz2  14749  ramz  14750  gex1  16933  sylow2a  16961  en1top  19776  en2top  19777  hmph0  20586  ptcmplem2  20843  dscmet  21383  dscopn  21384  xrge0tsms2  21630  htpycc  21770  pcohtpylem  21809  pcopt  21812  pcopt2  21813  pcoass  21814  pcorevlem  21816  vitalilem5  22311  dvef  22671  dveq0  22691  dv11cn  22692  deg1lt0  22781  ply1rem  22854  fta1g  22858  plyremlem  22990  aalioulem3  23020  pige3  23200  relogrn  23239  logneg  23265  cxpaddlelem  23419  mule1  23801  ppiub  23858  dchrabs2  23916  bposlem1  23938  lgseisen  24007  lgsquadlem2  24009  rpvmasumlem  24051  qabvle  24189  ostth3  24202  colinearalg  24617  eengstr  24687  konigsberg  25391  nmosetn0  26080  nmoo0  26106  siii  26168  bcsiALT  26496  branmfn  27423  esumrnmpt2  28501  ballotlemrc  28961  subfacval3  29473  sconpi1  29523  fz0n  29924  itg2addnclem  31419  ftc1anc  31451  radcnvrat  36023  stoweidlem18  37149  stoweidlem55  37186  fourierdlem62  37300  fourierswlem  37362  exple2lt6  38449
  Copyright terms: Public domain W3C validator