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

Theorem syl6eqssr 3521
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 2437 . 2  |-  ( ph  ->  A  =  B )
3 syl6eqssr.2 . 2  |-  B  C_  C
42, 3syl6eqss 3520 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  ffvresb  6069  tposss  6982  sbthlem5  7692  rankxpl  8345  winafp  9121  wunex2  9162  iooval2  11669  telfsumo  13840  structcnvcnv  15095  ressbasss  15143  tsrdir  16435  idrespermg  17003  symgsssg  17059  gsumzoppg  17512  opsrtoslem2  18643  dsmmsubg  19237  cnclsi  20219  txss12  20551  txbasval  20552  kqsat  20677  kqcldsat  20679  fmss  20892  cfilucfil  21505  tngtopn  21589  dvaddf  22773  dvmulf  22774  dvcof  22779  dvmptres3  22787  dvmptres2  22793  dvmptcmul  22795  dvmptcj  22799  dvcnvlem  22805  dvcnv  22806  dvcnvrelem1  22846  dvcnvrelem2  22847  plyrem  23126  ulmss  23217  ulmdvlem1  23220  ulmdvlem3  23222  ulmdv  23223  isppw  23904  dchrelbas2  24028  chsupsn  26901  pjss1coi  27651  off2  28082  resspos  28258  resstos  28259  submomnd  28311  suborng  28417  submatres  28471  madjusmdetlem2  28493  madjusmdetlem3  28494  omsmon  28959  signstfvn  29246  elmsta  29974  mthmpps  30008  dissneqlem  31476  hbtlem6  35694  dvmulcncf  37369  dvdivcncf  37371  itgsubsticclem  37421  lidlssbas  38680
  Copyright terms: Public domain W3C validator