![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pssssd | Structured version Unicode version |
Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.) |
Ref | Expression |
---|---|
pssssd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pssssd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pssssd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pssss 3562 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 |