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