Theorem sspsstr

Description: Transitive law for subclass and proper subclass. (Contributed by NM, 3-Apr-1996)

	Ref	Expression
Assertion	sspsstr	|- ( ( A C_ B /\ B C. C ) -> A C. C )

Proof

Step	Hyp	Ref	Expression
1		sspss	|- ( A C_ B <-> ( A C. B \/ A = B ) )
2		psstr	|- ( ( A C. B /\ B C. C ) -> A C. C )
3	2	ex	|- ( A C. B -> ( B C. C -> A C. C ) )
4		psseq1	|- ( A = B -> ( A C. C <-> B C. C ) )
5	4	biimprd	|- ( A = B -> ( B C. C -> A C. C ) )
6	3 5	jaoi	|- ( ( A C. B \/ A = B ) -> ( B C. C -> A C. C ) )
7	6	imp	|- ( ( ( A C. B \/ A = B ) /\ B C. C ) -> A C. C )
8	1 7	sylanb	|- ( ( A C_ B /\ B C. C ) -> A C. C )