theorem eqid (a: nat): $ a = a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imidm | (x = a -> x = a -> a = a) -> x = a -> a = a |
|
2 | ax_7 | x = a -> x = a -> a = a |
|
3 | 1, 2 | ax_mp | x = a -> a = a |
4 | 3 | eex | E. x x = a -> a = a |
5 | ax_6 | E. x x = a |
|
6 | 4, 5 | ax_mp | a = a |