theorem sbeq2i {x: nat} (a: nat x) (b c: wff x): $ b <-> c $ > $ [a / x] b <-> [a / x] c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | b <-> c |
|
2 | 1 | a1i | T. -> (b <-> c) |
3 | 2 | sbeq2d | T. -> ([a / x] b <-> [a / x] c) |
4 | 3 | trud | [a / x] b <-> [a / x] c |