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

Theorem syl6eqbr 4317
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 4290 . 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 1362   class class class wbr 4280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281
This theorem is referenced by:  syl6eqbrr  4318  domunsn  7449  mapdom1  7464  mapdom2  7470  pm54.43  8158  cdadom1  8343  infmap2  8375  inar1  8930  gruina  8973  xltnegi  11174  leexp1a  11906  discr  11985  facwordi  12049  faclbnd3  12052  hashsnlei  12154  hashgt12el  12157  cnpart  12713  geomulcvg  13319  dvds1  13564  ramz2  14068  ramz  14069  gex1  16070  sylow2a  16098  en1top  18431  en2top  18432  hmph0  19210  ptcmplem2  19467  dscmet  20007  dscopn  20008  xrge0tsms2  20254  htpycc  20394  pcohtpylem  20433  pcopt  20436  pcopt2  20437  pcoass  20438  pcorevlem  20440  vitalilem5  20934  dvef  21294  dveq0  21314  dv11cn  21315  deg1lt0  21447  ply1rem  21520  fta1g  21524  plyremlem  21655  aalioulem3  21685  pige3  21864  relogrn  21898  logneg  21921  cxpaddlelem  22074  mule1  22371  ppiub  22428  dchrabs2  22486  bposlem1  22508  lgseisen  22577  lgsquadlem2  22579  rpvmasumlem  22621  qabvle  22759  ostth3  22772  colinearalg  22979  eengstr  23049  konigsberg  23431  nmosetn0  23988  nmoo0  24014  siii  24076  bcsiALT  24404  branmfn  25332  ballotlemrc  26761  subfacval3  26925  sconpi1  26976  fz0n  27236  itg2addnclem  28287  ftc1anc  28319  stoweidlem18  29659  stoweidlem55  29696  exple2lt6  30598
  Copyright terms: Public domain W3C validator