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

Theorem syl6eqssr 3405
Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
syl6eqssr.1  |-  ( ph  ->  B  =  A )
syl6eqssr.2  |-  B  C_  C
Assertion
Ref Expression
syl6eqssr  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6eqssr
StepHypRef Expression
1 syl6eqssr.1 . . 3  |-  ( ph  ->  B  =  A )
21eqcomd 2446 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqssr.2 . 2  |-  B  C_  C
42, 3syl6eqss 3404 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3326
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 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-in 3333  df-ss 3340
This theorem is referenced by:  ffvresb  5872  tposss  6744  sbthlem5  7423  rankxpl  8080  winafp  8862  wunex2  8903  iooval2  11331  fsumtscopo  13263  structcnvcnv  14183  ressbasss  14228  tsrdir  15406  idrespermg  15914  symgsssg  15971  opsrtoslem2  17564  dsmmsubg  18166  cnclsi  18874  txss12  19176  txbasval  19177  kqsat  19302  kqcldsat  19304  fmss  19517  cfilucfilOLD  20142  cfilucfil  20143  tngtopn  20234  dvaddf  21414  dvmulf  21415  dvcof  21420  dvmptres3  21428  dvmptres2  21434  dvmptcj  21440  dvcnvlem  21446  dvcnv  21447  dvcnvrelem1  21487  dvcnvrelem2  21488  plyrem  21769  ulmss  21860  ulmdvlem1  21863  ulmdvlem3  21865  ulmdv  21866  isppw  22450  dchrelbas2  22574  chsupsn  24814  pjss1coi  25565  off2  25957  resspos  26118  resstos  26119  submomnd  26171  suborng  26281  omsmon  26709  signstfvn  26968  hbtlem6  29482
  Copyright terms: Public domain W3C validator