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