Theorem pssssd 4032

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

Syntax hints:   → wi 4   ⊆ wss 3887   ⊊ wpss 3888

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 397  df-pss 3906

This theorem is referenced by:  fin23lem36  10104  fin23lem39  10106  canthnumlem  10404  canthp1lem2  10409  elprnq  10747  npomex  10752  prlem934  10789  ltexprlem7  10798  wuncn  10926  mrieqv2d  17348  slwpss  19217  pgpfac1lem5  19682  lbspss  20344  lsppratlem1  20409  lsppratlem3  20411  lsppratlem4  20412  lrelat  37028  lsatcvatlem  37063