# Proving this sequent using natural deduction

I'm stuck on proving the following: $$\forall x(\phi \lor \psi) \vdash \forall x\phi \lor \psi$$ Here, $x$ is not free in $\psi$ but can be free in $\phi$. My proof starts like the following:

1. $\forall x(\phi \lor \psi)$ (premise)
2. $x_0$
3. $\phi[x_0/x] \lor \psi$
4. $\psi$ (assumption)
5. $\forall x\phi \lor \psi$ (or-introduction)
6. $\phi[x_0/x]$ (assumption)
7. ...

And then I'm stuck. In the proof it is like the or-context is in conflict with the $x_0$-context.

Brams28's answer looks correct. But I don't understand why there can't be a simpler proof. The analoguous sequent in propositional logic is just $(p_1 \lor q) \land (p_2 \lor q) \vdash (p_1 \land p_2) \lor q$ which is easily solvable without contradictions.

• The problem is that if the disjunction you have is inside a universal quantifier, so to get to the disjunction you need to instantiate it, but as soon as you do that, you lose the generality of the universal .. at least in the particular proof system I used here. – Bram28 Apr 1 '18 at 18:38