Theorem pssssd 3564

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 3562	. 2 |- ( A C. B -> A C_ B )
3	1, 2	syl 16	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   C_ wss 3439   C. wpss 3440

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