theorem nfx {x: nat} (a b: wff x): $ a <-> b $ > $ F/ x b $ > $ F/ x a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h1 | a <-> b |
|
| 2 | 1 | nfeqi | (F/ x a) <-> (F/ x b) |
| 3 | 2 | bi2i | (F/ x b) -> (F/ x a) |
| 4 | hyp h2 | F/ x b |
|
| 5 | 3, 4 | ax_mp | F/ x a |