Metamath Proof Explorer

Theorem difeq1i

Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002)

Ref Expression
Hypothesis difeq1i.1 A = B
Assertion difeq1i A C = B C


Step Hyp Ref Expression
1 difeq1i.1 A = B
2 difeq1 A = B A C = B C
3 1 2 ax-mp A C = B C