theorem sbqcom {x: nat} (a: nat) (b: wff x): $ a = x -> ([a / x] b <-> b) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom | a = x -> x = a |
|
2 | sbq | x = a -> (b <-> [a / x] b) |
|
3 | 1, 2 | rsyl | a = x -> (b <-> [a / x] b) |
4 | 3 | bicomd | a = x -> ([a / x] b <-> b) |