theorem cbvsb {x y: nat} (a: nat) (p: wff x) (q: wff y): $ x = y -> (p <-> q) $ > $ [a / x] p <-> [a / y] q $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv | F/ y p |
|
2 | nfv | F/ x q |
|
3 | hyp e | x = y -> (p <-> q) |
|
4 | 1, 2, 3 | cbvsbh | [a / x] p <-> [a / y] q |