Theorem ineq2

Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993)

	Ref	Expression
Assertion	ineq2	$$⊢A=B\to C\cap A=C\cap B$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=B\to A\cap C=B\cap C$$
2		incom	$$⊢C\cap A=A\cap C$$
3		incom	$$⊢C\cap B=B\cap C$$
4	1 2 3	3eqtr4g	$$⊢A=B\to C\cap A=C\cap B$$