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