Metamath Proof Explorer


Theorem difeq12d

Description: Equality deduction for class difference. (Contributed by FL, 29-May-2014)

Ref Expression
Hypotheses difeq12d.1 φ A = B
difeq12d.2 φ C = D
Assertion difeq12d φ A C = B D

Proof

Step Hyp Ref Expression
1 difeq12d.1 φ A = B
2 difeq12d.2 φ C = D
3 1 difeq1d φ A C = B C
4 2 difeq2d φ B C = B D
5 3 4 eqtrd φ A C = B D