I'm taking a first-order logic class and I keep finding myself stuck on proofs that ask for disjunction elimination and then supply additional premises with conjunctions. How can I eliminate negations and conjunctions to get the premises I need to get consistent conclusions in disjunction elimination subproofs? Here's an example of something I'm working on:
1.| SameRow(b,f) v SameRow(c,f) v SameRow(d,f)
4.| ~(SameRow(d,f) ∧ Cube(f))
| ⊥ Ana Con 3,5
|~Cube(f) ⊥Elim 6
| ⊥ ⊥Intro 2,8
|~Cube(f) ⊥Elim 9
At this point I'm not sure what to do about the SameRow(d,f) part of the disjunct in premise 1. How do I use ~(SameRow(d,f) ∧ Cube(f)) to derive anything that I can use to reach ~Cube(f) in the last subproof? I get that the sentence is equivalent to ~SameRow(d,f) ∧ ~Cube(f), but I can't see how to get a contradiction from that.
Any help about this problem/strategy in general would be much appreciated! Thank you.