Theorem pssssd 3998

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

Step	Hyp	Ref	Expression
1		pssssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊊ 𝐵)
2		pssss 3996	. 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3853   ⊊ wpss 3854

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 210  df-an 400  df-pss 3872

This theorem is referenced by:  fin23lem36  9860  fin23lem39  9862  canthnumlem  10160  canthp1lem2  10165  elprnq  10503  npomex  10508  prlem934  10545  ltexprlem7  10554  wuncn  10682  mrieqv2d  17025  slwpss  18867  pgpfac1lem5  19332  lbspss  19985  lsppratlem1  20050  lsppratlem3  20052  lsppratlem4  20053  lrelat  36683  lsatcvatlem  36718