Theorem bnj1241

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1241.1	|- ( ph -> A C_ B )
	bnj1241.2	|- ( ps -> C = A )
Assertion	bnj1241	|- ( ( ph /\ ps ) -> C C_ B )

Proof

Step	Hyp	Ref	Expression
1		bnj1241.1	|- ( ph -> A C_ B )
2		bnj1241.2	|- ( ps -> C = A )
3	2	eqcomd	|- ( ps -> A = C )
4	3	adantl	|- ( ( ph /\ ps ) -> A = C )
5	1	adantr	|- ( ( ph /\ ps ) -> A C_ B )
6	4 5	eqsstrrd	|- ( ( ph /\ ps ) -> C C_ B )