How to derive: $\left(\forall x\right)\left[Lx\rightarrow\left(Mx\land N x\right)\right]\vdash\left(\forall x\right)\left(Lx\rightarrow M x\right)$

Question

I'm trying to derive: $\left(\forall x\right)\left[Lx\rightarrow\left(Mx\land N x\right)\right]\vdash\left(\forall x\right)\left(Lx\rightarrow M x\right)$

I thought I was on the right track with:

$1 \hspace{5 mm}(1) \left(\forall x\right)\left[Lx\rightarrow\left(Mx\land N x\right)\right]\hspace{10 mm}A\\ 1\hspace{5 mm}(2)\hspace{10 mm} La\rightarrow\left(Ma\land N a\right) \ \hspace{8 mm}1,\forall E\\ 2\hspace{5 mm}(3)\hspace{10 mm} La \hspace{42 mm}A\\ 2\hspace{5 mm}(4)\hspace{10 mm} Ma\ \land Na \ \hspace{20 mm}2,3\rightarrow E\\ 2\hspace{5 mm}(5)\hspace{10 mm} Ma \hspace{40 mm}4, \land E4\\ 1,2\hspace{1 mm}(6)\hspace{10 mm} La\rightarrow Ma \hspace{23 mm}2,4\rightarrow I\\ 1,2\hspace{5 mm}(7)\hspace{10 mm} \left(\forall x\right)\left(Lx\rightarrow M x\right) \hspace{10 mm}6, \forall I\\ $

However, I think by assuming the antecedent in step (3) that I've done something wrong. Is that step allowed or is there a more efficient way to derive the conclusion? Or can anyone provide any insights that I may have missed?

Answer 1

Your derivation is all correct; well done!

The assumption in (3) is unproblematic because the $\to I$ rule in step 6 allows to discharges this assumption: When using $\to I$ to turn the assumption from which the succedent was derived into the antecedent of a conditional, that assumption can be dropped because the conclusion no longer depends on the truth of that assumption.

Answer 2

Here is another approach (convenient if you doubt about the introduction of arbitrary assumptions):

$$ \begin{array}{lll} (1)&(\forall x)[Lx\to(Mx\land Nx)]&\text{Premise}\\ (2)&La\to(Ma\land Na)&\text{\(\forall\) elimination (1)}\\ (3)&\neg La\lor(Ma\land Na)&\text{\(\to\) equivalence (2)}\\ (4)&(\neg La\lor Ma)\land(\neg La\lor Na)&\text{\(\lor\) distributive (3)}\\ (5)&\neg La\lor Ma&\text{\(\land\) elimination (4)}\\ (6)&La\to Ma&\text{\(\to\) equivalence (5)}\\ (7)&(\forall x)(Lx\to Mx)&\text{\(\forall\) introduction (6)}\\ \end{array} $$