Theorem pssssd 4095

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 4093	. 2 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3947   ⊊ wpss 3948

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 395  df-pss 3966

This theorem is referenced by:  fin23lem36  10377  fin23lem39  10379  canthnumlem  10677  canthp1lem2  10682  elprnq  11020  npomex  11025  prlem934  11062  ltexprlem7  11071  wuncn  11199  mrieqv2d  17624  slwpss  19572  pgpfac1lem5  20041  lbspss  20972  lsppratlem1  21040  lsppratlem3  21042  lsppratlem4  21043  lrelat  38490  lsatcvatlem  38525  oaun3lem1  42806  oaun3lem2  42807