Theorem pssssd 3537

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

Step	Hyp	Ref	Expression
1		pssssd.1	. 2 |- ( ph -> A C. B )
2		pssss 3535	. 2 |- ( A C. B -> A C_ B )
3	1, 2	syl 17	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   C_ wss 3411   C. wpss 3412

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 369  df-pss 3427

This theorem is referenced by:  fin23lem36  8678  fin23lem39  8680  canthnumlem  8974  canthp1lem2  8979  elprnq  9317  npomex  9322  prlem934  9359  ltexprlem7  9368  wuncn  9495  mrieqv2d  15143  slwpss  16846  pgpfac1lem5  17340  lbspss  17938  lsppratlem1  18003  lsppratlem3  18005  lsppratlem4  18006  lrelat  31996  lsatcvatlem  32031