find formal proof for a simple tautology [on hold]

Could you please help me figure out the formal proof for the following argument? This is an example from the textbook "Language, proof and logic" (by D. Barker-Plummer et al). I am doing it in the program called Fitch.

$$\begin{array}{r} A\land (B\lor C)\\ \hline (A\land B) \lor (A\land C) \end{array}$$

The answer is obvious, if you formulate an informal proof, but I can't get it right formally. The screenshot below shows exactly where I've got stuck...

Any hints will be greatly appreciated! Thank you!

-

put on hold as off-topic by Najib Idrissi, Adriano, Giuseppe Negro, 5xum, Daniel Fischeryesterday

This question appears to be off-topic. The users who voted to close gave this specific reason:

• "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Najib Idrissi, Adriano, Giuseppe Negro, 5xum, Daniel Fischer
If this question can be reworded to fit the rules in the help center, please edit the question.

This is now the third of these questions that you're posting. a) It would be good style to link them to each other so people can build on the effort that's already been put into figuring out what formal system you're using etc. b) Three very specific very similar homework questions seems a bit much -- if the answers to the other two haven't helped you with this one, perhaps you should try to figure out on a more general level which piece of insight you're missing for doing these? –  joriki Dec 15 '11 at 0:15
What rules are we using? –  simplicity Dec 15 '11 at 0:35
I think you refer to this text, but I'm not sure it's the same edition ssdi.di.fct.unl.pt/~pb/cadeiras/lc/0102/lpl%20textbook.pdf Note 5. isn't correct, because you haven't derived "C". –  Doug Spoonwood Dec 15 '11 at 2:53
And after four question you still have not disclosed which rules you're using. Are you reading the comments at all? –  Henning Makholm Dec 15 '11 at 3:55

You have (B v C) in step 3. If you reread the section on the V-elimination rule, it says something like "from (P v Q), a subproof which starts with P and ends with Z, and a subproof which starts with Q and ends with Z, we can infer Z." (I've only scanned that text, but it more-or-less says that, I think). So, if you can do so, it would work out well to start with B and show that it leads to ((A∧B)∨(A∧C)), then you'd start with C and show that it leads to ((A∧B)∨(A∧C)). Now, you have A from step 2 validly inferred by ^ elimination. So, if you have A, and you've assumed B, what can you infer under the scope of assumption B? Then note what the conclusion comes as. It consists of a disjunction. What rule do you have for getting to a disjunction? In other words, what rule do you have for inferring to a disjunction? Do you have "half of" that disjunction (in other words... do you have either the first or the second disjunct?)? If you have A, and you've assumed C, what can you infer under the scope of assumption C? Can you link this with the conclusion also?

Does that help enough?

-