I am trying to use existential elimination to derive Brillig(a) & Tove(a). how would I do this? I have tried to do separate sub proofs to prove both Brillig(a) & Tove(a) but that doesn't work either. Can someone point me in the right direction?
The reason you are having trouble doing that, is that that can not be done.
It is not a valid derivation. The conjunction of two existences does not entail an existence of a conjunction.
Neither do the other two premises enable it to be derived.
PS: Existential Elimination requires an existential statement, and the assumption of a witness for that existence, under which is derived a statement that does not freely contain the witness variable.
i| Ǝx T(x) Derived or Premised j| |_ [a] T(a) Assumption (of a witness for i) | | : k| | S Derived Somehow; S does not contain the witness variable | S Ǝ Elimination i,j-k