theorem eqerd (G: wff) (a: nat) (p: wff) {x: nat}: $ G -> a = x -> p $ > $ G -> p $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax_6 | E. x x = a |
|
2 | eqcom | x = a -> a = x |
|
3 | hyp h | G -> a = x -> p |
|
4 | 2, 3 | syl5 | G -> x = a -> p |
5 | 4 | eexd | G -> E. x x = a -> p |
6 | 1, 5 | mpi | G -> p |