Premise: A v (B ^C)
Premise: ~B v ~C v D
Goal: A v D
Prove it formally without using DeMorgan's Law.
1.A v (B ^C)
2.~B v ~C v D
4.-A V D (V intro 3)
--7. B (conjunction elim. 5)
--8. contradiction (contradiction intro 6&7)
--9. A V D (contradiction intro)
--11. C (conjunction elim. 5)
--12. contradiction (c intro 11&12)
--13. A V D (contradiction elim)
You do the rest! If you can get A V D on the second level of the subproof, you can bring it to the first by means of disjunction elim. Once you do that, the rest should be easy!
The OP would like a formal proof of the following:
Premise: A ∨ (B ∧ C)
Premise: ¬B ∨ ¬C ∨ D
Goal: A ∨ D
The first thing to note is that although it looks like the second premise is a symbolization of something, it is not a valid sentence. It is only an expression. The scope of the connectives, "∨", is ambiguous. To make this a sentence that we can use formally it needs to be rewritten as either
(¬B ∨ ¬C) ∨ D
¬B ∨ (¬C ∨ D)
To see this try putting the expression ¬B ∨ ¬C ∨ D into a proof checker. Can one even get started? This is what happened when I tried using the natural deduction and proof checker used by forall x: Calgary Remix:
Based on our human understanding of the connective "∨" as "or" we could proceed informally to use the expression as it is and think that we are doing cases. First we would consider the case "¬B", then the case "¬C" and then the case D and see if we can get to the goal "A ∨ D" in each case.
However, since we want a formal proof, we can't proceed in that manner. We need to use sentences, not arbitrary expressions, no matter how obvious they are to us, and we need to use formal rules for disjunctions (that is, "∨") to justify each line of the formal proof. A proof checker helps us verify that we are using sentences and following the rules.
If we choose ~B v (~C v D) as the sentence, we can get a proof like the following.
This proof shows a way to handle the cases in both of the premises by formally eliminating the "V" connective through subproofs.
Consider the two cases in the first premise. I assume, that is, start a subproof with "A" as an assumption on line 3 and reach the desired goal on line 4 and I assume "(B ∧ C)" on line 5 and reach the desired goal on line 18. With both sides of the "V" connective reaching the goal, I can eliminate the "V" and complete the proof. This elimination discharges the two assumptions I made represented by the two subproofs, one for each case.
The second case above required more lines. Let's consider those details. To reach the goal for the second case, "(B ∧ C)", I needed to use the second premise. I assumed the "¬B" case by creating a subproof with "¬B" as an assumption on line 7 and reached the goal on line 9 and I assumed the "¬C ∨ D" case on line 10 and reached the conclusion on line 17. Note that "¬C ∨ D" is also a disjunction, a "∨" sentence, and so I need to use cases, that is, subproofs, on it as well. I did this on lines 10 through 17.
One of the requirements in the OP was:
Prove it formally without using DeMorgan's Law
Note that I did not use DeMorgan's Law in the proof above. To see how DeMorgan's Law might have been used consider the following proof using "(¬B ∨ ¬C) ∨ D".
I did it, but the proof is monstrously long. If anyone knows how to simplify it I would appreciate it. Done with Stanford's Fitch proof editor: