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

Theorem syl6eqssr 3367
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 2417 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqssr.2 . 2  |-  B  C_  C
42, 3syl6eqss 3366 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3288
This theorem is referenced by:  ffvresb  5867  tposss  6447  sbthlem5  7188  rankxpl  7765  winafp  8536  wunex2  8577  iooval2  10913  fsumtscopo  12544  structcnvcnv  13443  ressbasss  13484  tsrdir  14646  opsrtoslem2  16508  cnclsi  17298  txss12  17598  txbasval  17599  kqsat  17724  kqcldsat  17726  fmss  17939  cfilucfilOLD  18560  cfilucfil  18561  tngtopn  18652  dvaddf  19789  dvmulf  19790  dvcof  19795  dvmptres3  19803  dvmptres2  19809  dvmptcj  19815  dvcnvlem  19821  dvcnv  19822  dvcnvrelem1  19862  dvcnvrelem2  19863  plyrem  20183  ulmss  20274  ulmdvlem1  20277  ulmdvlem3  20279  ulmdv  20280  isppw  20858  dchrelbas2  20982  chsupsn  22876  pjss1coi  23627  off2  24015  resspos  24148  resstos  24149  subofld  24206  mblfinlem  26151  dsmmsubg  27085  hbtlem6  27209  symgsssg  27284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator