Description: Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | deceq1i.1 | ⊢ 𝐴 = 𝐵 | |
Assertion | deceq1i | ⊢ ; 𝐴 𝐶 = ; 𝐵 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | deceq1i.1 | ⊢ 𝐴 = 𝐵 | |
2 | deceq1 | ⊢ ( 𝐴 = 𝐵 → ; 𝐴 𝐶 = ; 𝐵 𝐶 ) | |
3 | 1 2 | ax-mp | ⊢ ; 𝐴 𝐶 = ; 𝐵 𝐶 |