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

Theorem pssssd 3682
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 3680 . 2 (𝐴𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3555  wpss 3556
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 197  df-an 386  df-pss 3571
This theorem is referenced by:  fin23lem36  9114  fin23lem39  9116  canthnumlem  9414  canthp1lem2  9419  elprnq  9757  npomex  9762  prlem934  9799  ltexprlem7  9808  wuncn  9935  mrieqv2d  16220  slwpss  17948  pgpfac1lem5  18399  lbspss  19001  lsppratlem1  19066  lsppratlem3  19068  lsppratlem4  19069  lrelat  33778  lsatcvatlem  33813
  Copyright terms: Public domain W3C validator