theorem sbthd (G: wff) (a: nat) {x: nat} (p: wff x): $ G /\ x = a -> p $ > $ G -> [a / x] p $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | itru | T. |
|
2 | bith | p -> T. -> (p <-> T.) |
|
3 | 1, 2 | mpi | p -> (p <-> T.) |
4 | hyp h | G /\ x = a -> p |
|
5 | 3, 4 | syl | G /\ x = a -> (p <-> T.) |
6 | 5 | sbed | G -> ([a / x] p <-> T.) |
7 | 1, 6 | mpbiri | G -> [a / x] p |