Hey, If anyone here likes working on these problems, I'm working on a couple more. I finished the first two. These go: 1. Vx Vy (Fxy ---> ~Fyx) |- -ExFxx (now my work - maybe wrong 2. Vy (Fay ---> ~Fya) 1,VE 3. (Faa ---> ~Faa) 2,VE 4. | Faa H(for -->E) 5. | ~Faa 3,4, CON 6. Faa 7. ~~Faa 3,6, MT (I find this hard to articulate in the logical format, but basically, if ~Faa is proved wrong by Faa in line six(~(~Faa)), then MT says that ~Faa can be infered...) 8. ~Faa 9. -ExFxx 8, EI(can I do this?) Actually ended up working it out as I posted it. Is it right, though? Btw, does anyone know the tex way to do this? Test: [tex]VxEy(Mxy -> Fxy) [/tex] Didn't work.