theorem sbeh {x: nat} (a: nat) (b c: wff x):
$ F/ x c $ >
$ x = a -> (b <-> c) $ >
$ [a / x] b <-> c $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | F/ x c |
|
| 2 | 1 | sbeht | A. x (x = a -> (b <-> c)) -> ([a / x] b <-> c) |
| 3 | hyp e | x = a -> (b <-> c) |
|
| 4 | 3 | ax_gen | A. x (x = a -> (b <-> c)) |
| 5 | 2, 4 | ax_mp | [a / x] b <-> c |