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

Theorem pssssd 3564
Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
Hypothesis
Ref Expression
pssssd.1  |-  ( ph  ->  A  C.  B )
Assertion
Ref Expression
pssssd  |-  ( ph  ->  A  C_  B )

Proof of Theorem pssssd
StepHypRef Expression
1 pssssd.1 . 2  |-  ( ph  ->  A  C.  B )
2 pssss 3562 . 2  |-  ( A 
C.  B  ->  A  C_  B )
31, 2syl 16 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3439    C. wpss 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-pss 3455
This theorem is referenced by:  fin23lem36  8631  fin23lem39  8633  canthnumlem  8929  canthp1lem2  8934  elprnq  9274  npomex  9279  prlem934  9316  ltexprlem7  9325  wuncn  9451  mrieqv2d  14699  slwpss  16235  pgpfac1lem5  16705  lbspss  17289  lsppratlem1  17354  lsppratlem3  17356  lsppratlem4  17357  lrelat  33017  lsatcvatlem  33052
  Copyright terms: Public domain W3C validator