Metamath Proof Explorer


Theorem difeq12

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

Ref Expression
Assertion difeq12 A=BC=DAC=BD

Proof

Step Hyp Ref Expression
1 difeq1 A=BAC=BC
2 difeq2 C=DBC=BD
3 1 2 sylan9eq A=BC=DAC=BD