Theorem pssssd 4028

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

Syntax hints:   → wi 4   ⊆ wss 3883   ⊊ wpss 3884

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 396  df-pss 3902

This theorem is referenced by:  fin23lem36  10035  fin23lem39  10037  canthnumlem  10335  canthp1lem2  10340  elprnq  10678  npomex  10683  prlem934  10720  ltexprlem7  10729  wuncn  10857  mrieqv2d  17265  slwpss  19132  pgpfac1lem5  19597  lbspss  20259  lsppratlem1  20324  lsppratlem3  20326  lsppratlem4  20327  lrelat  36955  lsatcvatlem  36990