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

Theorem pssssd 3901
Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
Hypothesis
Ref Expression
pssssd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
pssssd (𝜑𝐴𝐵)

Proof of Theorem pssssd
StepHypRef Expression
1 pssssd.1 . 2 (𝜑𝐴𝐵)
2 pssss 3899 . 2 (𝐴𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3769  wpss 3770
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 199  df-an 386  df-pss 3785
This theorem is referenced by:  fin23lem36  9458  fin23lem39  9460  canthnumlem  9758  canthp1lem2  9763  elprnq  10101  npomex  10106  prlem934  10143  ltexprlem7  10152  wuncn  10279  mrieqv2d  16614  slwpss  18340  pgpfac1lem5  18794  lbspss  19403  lsppratlem1  19470  lsppratlem3  19472  lsppratlem4  19473  lrelat  35035  lsatcvatlem  35070
  Copyright terms: Public domain W3C validator