theorem iexeh {x: nat} (a: nat) (b c: wff x):
$ F/ x c $ >
$ x = a -> (b <-> c) $ >
$ c -> E. x b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax_6 | E. x x = a |
|
| 2 | exim | A. x (x = a -> b) -> E. x x = a -> E. x b |
|
| 3 | hyp h | F/ x c |
|
| 4 | hyp e | x = a -> (b <-> c) |
|
| 5 | 4 | bi2d | x = a -> c -> b |
| 6 | 5 | com12 | c -> x = a -> b |
| 7 | 3, 6 | ialdh | c -> A. x (x = a -> b) |
| 8 | 2, 7 | syl | c -> E. x x = a -> E. x b |
| 9 | 1, 8 | mpi | c -> E. x b |