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

Theorem pssssd 4062
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 4060 . 2 (𝐴𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3915  wpss 3916
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 206  df-an 398  df-pss 3934
This theorem is referenced by:  fin23lem36  10291  fin23lem39  10293  canthnumlem  10591  canthp1lem2  10596  elprnq  10934  npomex  10939  prlem934  10976  ltexprlem7  10985  wuncn  11113  mrieqv2d  17526  slwpss  19401  pgpfac1lem5  19865  lbspss  20559  lsppratlem1  20624  lsppratlem3  20626  lsppratlem4  20627  lrelat  37505  lsatcvatlem  37540  oaun3lem1  41719  oaun3lem2  41720
  Copyright terms: Public domain W3C validator