theorem sbneq1d {x: nat} (G: wff x) (a b c: nat x): $ G -> a = b $ > $ G -> N[a / x] c = N[b / x] c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbneq1 | a = b -> N[a / x] c = N[b / x] c |
|
2 | hyp h | G -> a = b |
|
3 | 1, 2 | syl | G -> N[a / x] c = N[b / x] c |