Theorem sstri

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000)

	Ref	Expression
Hypotheses	sstri.1	|- A C_ B
	sstri.2	|- B C_ C
Assertion	sstri	|- A C_ C

Proof

Step	Hyp	Ref	Expression
1		sstri.1	|- A C_ B
2		sstri.2	|- B C_ C
3		sstr2	|- ( A C_ B -> ( B C_ C -> A C_ C ) )
4	1 2 3	mp2	|- A C_ C