Theorem psssstr

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

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

Proof

Step	Hyp	Ref	Expression
1		sspss	|- ( B C_ C <-> ( B C. C \/ B = C ) )
2		psstr	|- ( ( A C. B /\ B C. C ) -> A C. C )
3	2	ex	|- ( A C. B -> ( B C. C -> A C. C ) )
4		psseq2	|- ( B = C -> ( A C. B <-> A C. C ) )
5	4	biimpcd	|- ( A C. B -> ( B = C -> A C. C ) )
6	3 5	jaod	|- ( A C. B -> ( ( B C. C \/ B = C ) -> A C. C ) )
7	6	imp	|- ( ( A C. B /\ ( B C. C \/ B = C ) ) -> A C. C )
8	1 7	sylan2b	|- ( ( A C. B /\ B C_ C ) -> A C. C )