Theorem pssssd 4075

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

Syntax hints:   → wi 4   ⊆ wss 3926   ⊊ wpss 3927

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 207  df-an 396  df-pss 3946

This theorem is referenced by:  fin23lem36  10362  fin23lem39  10364  canthnumlem  10662  canthp1lem2  10667  elprnq  11005  npomex  11010  prlem934  11047  ltexprlem7  11056  wuncn  11184  mrieqv2d  17651  slwpss  19593  pgpfac1lem5  20062  lbspss  21040  lsppratlem1  21108  lsppratlem3  21110  lsppratlem4  21111  hashpss  32788  exsslsb  33636  lrelat  39032  lsatcvatlem  39067  oaun3lem1  43398  oaun3lem2  43399