Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | oveq1i.1 | $${\u22a2}{A}={B}$$ | |
Assertion | oveqi | $${\u22a2}{C}{A}{D}={C}{B}{D}$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1i.1 | $${\u22a2}{A}={B}$$ | |
2 | oveq | $${\u22a2}{A}={B}\to {C}{A}{D}={C}{B}{D}$$ | |
3 | 1 2 | ax-mp | $${\u22a2}{C}{A}{D}={C}{B}{D}$$ |