Theorem sseldd

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004)

	Ref	Expression
Hypotheses	sseld.1	|- ( ph -> A C_ B )
	sseldd.2	|- ( ph -> C e. A )
Assertion	sseldd	|- ( ph -> C e. B )

Proof

Step	Hyp	Ref	Expression
1		sseld.1	|- ( ph -> A C_ B )
2		sseldd.2	|- ( ph -> C e. A )
3	1	sseld	|- ( ph -> ( C e. A -> C e. B ) )
4	2 3	mpd	|- ( ph -> C e. B )