Metamath Proof Explorer


Theorem ineq12

Description: Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994)

Ref Expression
Assertion ineq12 A = B C = D A C = B D

Proof

Step Hyp Ref Expression
1 ineq1 A = B A C = B C
2 ineq2 C = D B C = B D
3 1 2 sylan9eq A = B C = D A C = B D