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 |
A. x (x = a -> (b <-> c)) -> ([a / x] b <-> c) |
||
3 |
hyp e |
x = a -> (b <-> c) |
|
4 |
A. x (x = a -> (b <-> c)) |
||
5 |
[a / x] b <-> c |