Metamath Proof Explorer


Theorem difeq12

Description: Equality theorem for class difference. (Contributed by FL, 31-Aug-2009)

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

Proof

Step Hyp Ref Expression
1 difeq1 A = B A C = B C
2 difeq2 C = D B C = B D
3 1 2 sylan9eq A = B C = D A C = B D