theorem sbth {x: nat} (a: nat x) (p: wff x): $ p $ > $ [a / x] p $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | p |
|
| 2 | 1 | a1i | x = y -> p |
| 3 | 2 | ax_gen | A. x (x = y -> p) |
| 4 | 3 | a1i | y = a -> A. x (x = y -> p) |
| 5 | 4 | ax_gen | A. y (y = a -> A. x (x = y -> p)) |
| 6 | 5 | conv sb | [a / x] p |