Theorem psstr

Description: Transitive law for proper subclass. Theorem 9 of Suppes p. 23. (Contributed by NM, 7-Feb-1996)

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

Proof

Step	Hyp	Ref	Expression
1		pssss	|- ( A C. B -> A C_ B )
2		pssss	|- ( B C. C -> B C_ C )
3	1 2	sylan9ss	|- ( ( A C. B /\ B C. C ) -> A C_ C )
4		pssn2lp	|- -. ( C C. B /\ B C. C )
5		psseq1	|- ( A = C -> ( A C. B <-> C C. B ) )
6	5	anbi1d	|- ( A = C -> ( ( A C. B /\ B C. C ) <-> ( C C. B /\ B C. C ) ) )
7	4 6	mtbiri	|- ( A = C -> -. ( A C. B /\ B C. C ) )
8	7	con2i	|- ( ( A C. B /\ B C. C ) -> -. A = C )
9		dfpss2	|- ( A C. C <-> ( A C_ C /\ -. A = C ) )
10	3 8 9	sylanbrc	|- ( ( A C. B /\ B C. C ) -> A C. C )