Natural Deduction proof: C Ʌ D, C ↔ E |- (C V F) Ʌ (D V F) Ʌ (E V F)

Question

This is one of the tasks that I'm working on in Logic class of a CS degree program at University.

The teacher just said to me that my answer was wrong, but she never told me when I asked her where I made a mistake. All she says is "You are not using the logical rules correctly, review it and fix the mistakes"

The below is my answer.

1 C Ʌ D Premise

2 C ↔ E Premise

3 C 1 (VE)

4 D 1 (VE)

5 C -> E 2 (↔E)

6 (C V F) Ʌ (D V F) Ʌ (E V F) 3, 4, 5 (ɅI)

I realized that the part "1 (VE)" for 3 and 4 should have been "1 (ɅE)", but can't really tell what other mistakes are left.

Any suggestion for correction, please?

** I attached a screenshot so it'll be easier to read.

screenshot

Revised version

Answer 1

1. As you already figured out, steps 3 and 4 are applications of $\land E$, not $\lor E$.
2. In step 5 when you apply the $\leftrightarrow E$ rule, your conclusion is not the implication $C \to E$, but the proposition $E$. The point of $\leftrightarrow E$ (at least by all the formulations of the rule that I am aware of, but that depends on what particular rule set you are using) is that given $A \leftrightarrow B$ and $A$, you can conclude $B$ and vice versa, i.e. exchange one formula for the other. Alternatively, if $\leftrightarrow E$ indeed gives you only the implication for one direction ($C \to E$), you would in addition have to apply $\to E$ together with $C$ to obtain $E$, since $E$ is the formula you need to construct $E \lor F$.
3. You can't just mash together multiple rule applications in one line, as you did in line 6:
   First derive each of the disjunctions $C \lor F, D \lor F, E \lor F$ individually by three applications of $\lor I$. Then introduce the conjunction in two $\land I$ steps: First $(C \lor F) \land (D \lor F)$, then $((C \lor F) \land (D \lor F)) \land (E \lor F)$.

With this, your proof should be as follows:

(produced with the Natural deduction proof editor and checker)

Answer 2

I think that this is an exhaustive list of your errors:

as you already realized 3 and 4 are really instances of conjunction elimination, and not disjunction elimination.

By the definition of the biconditional 5 can be thought of as another instance of conjunction elimination (I've never seen a rule like "biconditional elimination", not even in advanced textbooks on proof theory so I can't say whether you applied it correctly, I suspect it's like a modus ponens for the biconditional but there's no need for it)

You're missing an instance of modus ponens to go from $C \rightarrow E$ to $E$.

You skipped the 3 disjunction introduction to obtain formulae like $\;C\vee F$.

The revised version is better but you should introduce the disjunctions first on the three formulae, and then the final conjunction. (To be overly pedantic there should be two uses of conjunction introduction at the end).