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