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

Theorem syl6eqssr 3401
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 2443 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqssr.2 . 2  |-  B  C_  C
42, 3syl6eqss 3400 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  ffvresb  5903  tposss  6483  sbthlem5  7224  rankxpl  7804  winafp  8577  wunex2  8618  iooval2  10954  fsumtscopo  12586  structcnvcnv  13485  ressbasss  13526  tsrdir  14688  opsrtoslem2  16550  cnclsi  17341  txss12  17642  txbasval  17643  kqsat  17768  kqcldsat  17770  fmss  17983  cfilucfilOLD  18604  cfilucfil  18605  tngtopn  18696  dvaddf  19833  dvmulf  19834  dvcof  19839  dvmptres3  19847  dvmptres2  19853  dvmptcj  19859  dvcnvlem  19865  dvcnv  19866  dvcnvrelem1  19906  dvcnvrelem2  19907  plyrem  20227  ulmss  20318  ulmdvlem1  20321  ulmdvlem3  20323  ulmdv  20324  isppw  20902  dchrelbas2  21026  chsupsn  22920  pjss1coi  23671  off2  24059  resspos  24192  resstos  24193  subofld  24250  dsmmsubg  27200  hbtlem6  27324  symgsssg  27399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator