theorem nfeqd (_G: wff) {x: nat} (_a1 _a2: wff x):
$ _G -> (_a1 <-> _a2) $ >
$ _G -> ((F/ x _a1) <-> (F/ x _a2)) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp _ah | _G -> (_a1 <-> _a2) |
|
| 2 | 1 | aleqd | _G -> (A. x _a1 <-> A. x _a2) |
| 3 | 1, 2 | imeqd | _G -> (_a1 -> A. x _a1 <-> _a2 -> A. x _a2) |
| 4 | 3 | aleqd | _G -> (A. x (_a1 -> A. x _a1) <-> A. x (_a2 -> A. x _a2)) |
| 5 | 4 | conv nf | _G -> ((F/ x _a1) <-> (F/ x _a2)) |