theorem sbethh (a: nat) {x: nat} (p q: wff x): $ F/ x q $ > $ p $ > $ x = a -> (p <-> q) $ > $ q $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | F/ x q |
|
2 | hyp e | x = a -> (p <-> q) |
|
3 | 1, 2 | sbeh | [a / x] p <-> q |
4 | hyp hp | p |
|
5 | 4 | sbth | [a / x] p |
6 | 3, 5 | mpbi | q |