Theorem pssssd 3834

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

Syntax hints:   → wi 4   ⊆ wss 3703   ⊊ wpss 3704

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 197  df-an 385  df-pss 3719

This theorem is referenced by:  fin23lem36  9333  fin23lem39  9335  canthnumlem  9633  canthp1lem2  9638  elprnq  9976  npomex  9981  prlem934  10018  ltexprlem7  10027  wuncn  10154  mrieqv2d  16472  slwpss  18198  pgpfac1lem5  18649  lbspss  19255  lsppratlem1  19320  lsppratlem3  19322  lsppratlem4  19323  lrelat  34773  lsatcvatlem  34808