Check my proof:

UD:
Ex - x exists
Gx - x is God
Px - x is perfect
Qx - x is Q (you know, like in Bond or Star Trek?)
a - anchovies

1. |(Ex)(Gx -> Px) A
2. |(Ax)(Px -> Ex) A
--------------------
3. | |~Pa A
| ------
4. | | |~Qa A
| | ------
5. | | | |Qa A
| | | -----
6. | | | |~Qa R4
7. | | |Qa ~E5-6
8. | |Qa R7
9. | |~Qa R4
10.| Pa ~E3-9
11.|Pa -> Ea AE2
12.|Ea ->E10,11
13.||Ga -> Pa A
| ---------
14.| | |~Ga A
| | ------
15.| | | |~Qa A
| | | ------
16.| | | | |Qa A
| | | | ----
17.| | | | |~Qa R14
18.| | | |Qa ~E15-17
19.| | |Qa R16
20.| | |~Qa R15
21.| |Ga ~E14-20
22.| |Pa ->E12,18
23.|~Ga -> ~Pa EE13-22
24.||Ga A
| ---
25.||Ea R11
26.|Ga -> Ea ->I24-25
27.|(Ex)(Gx -> Ex) EI23

Obviously, this is the ontological argument. But after I did this proof, I figured out a simpler proof for this argument:

UD:
Ex - x exists
Px - x is perfect
g - God

1.|Pg A
2.|(Ax)(Px -> Ex) A
-----------------
3.|Pg -> Eg AE2
4.|Pg R1
5.|Eg ->E3,4

1. Ǝx(Gx -> Px)
2. ∀x(Px -> Ex)
ergo (Ǝx)(Gx -> Px)


First problem is that this argument begs the question. Assumption 1 is your conclusion, unless the parenthesis around your Ǝx makes the conclusion different from 1. But from my understanding, it shouldn't. All you really need to do is use a reiteration rule or a copy rule.

Do you mean to say?

1. Ǝx(Gx -> Px)
2. ∀x(Px -> Ex)
ergo (Ǝx)(Gx -> Ex)

---

1. Ǝx(Gx -> Px) | A
2. ∀x(Px -> Ex) | A
3. Negated conclusion | Provisional Assumption
4. Ax-(Gx -> Ex) | Quantifier Exchange, 3
5. Ga -> Pa | Existential Out, 1
6. -(Ga -> Ea) | Universal Out, 4
7. Pa -> Ea | Universal Out, 2
8. Ga . -Ea | Arrow Rule, 6
9. Pa | Modus Ponens, 5, 8 (one of the conjunctions)
10. Ea | Modus Ponens, 7, 9
11. -Ea | Conjunction out, 8
12. Ea . -Ea | Conjunction in, 10, 11
ergo (Ǝx)(Gx -> Ex) | Reductio ad absurdum or indirect proof

But even then, I thought existential statements were supposed to have conjunction symbols between the terms, not implication symbols.

Yes actually. Thanks for pointing out the typo. If God is perfection, and perfection entails existence, then God must exist is the common ontological argument, put forth by Descartes in his Meditations on First Philosophy.

As for the second rule, I didn't see anything to that effect in my logic book...

A > P | Premise
A & -P | PA
P | MP
-P | Conj out
P & -P | Conj in
-(A & -P) | Reductio

-(A & -P) | Premise
A | PA
-P |PA
A&-P | Conj in
-(A&-P)&(A&-P) | Conj in
P | Reductio
A > P | Conditional proof

Logically equivalent, bada bing.

Awesome. I can't think in math so trying to do these things always gives me headaches.

I take shortcuts, to be fair.

Usually when we see A&B and A>C, instead of doing the conjunctive elimination to get the antecedent of A>C, I just do Modus Ponens on A&B and A>C to get C, the consequent.

It should look like
1. A&B | Premise
2. A>C | Premise
3. A | Conjunction out, 1
4. C | Modus Ponens, 2, 3

But I do
1. A&B
2. A>C
3. C Modus Ponens, 2, 1

This way has the potential to lead to error/confusion, but for simple problems...so? The other counter might be that it's inelegant; again, so?