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

Theorem syl6eqssr 3391
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 2440 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqssr.2 . 2  |-  B  C_  C
42, 3syl6eqss 3390 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  ffvresb  5892  tposss  6472  sbthlem5  7213  rankxpl  7793  winafp  8564  wunex2  8605  iooval2  10941  fsumtscopo  12573  structcnvcnv  13472  ressbasss  13513  tsrdir  14675  opsrtoslem2  16537  cnclsi  17328  txss12  17629  txbasval  17630  kqsat  17755  kqcldsat  17757  fmss  17970  cfilucfilOLD  18591  cfilucfil  18592  tngtopn  18683  dvaddf  19820  dvmulf  19821  dvcof  19826  dvmptres3  19834  dvmptres2  19840  dvmptcj  19846  dvcnvlem  19852  dvcnv  19853  dvcnvrelem1  19893  dvcnvrelem2  19894  plyrem  20214  ulmss  20305  ulmdvlem1  20308  ulmdvlem3  20310  ulmdv  20311  isppw  20889  dchrelbas2  21013  chsupsn  22907  pjss1coi  23658  off2  24046  resspos  24179  resstos  24180  subofld  24237  mblfinlem  26234  dsmmsubg  27177  hbtlem6  27301  symgsssg  27376
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 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator