Inference in Predicate Logic I have stumbled upon the following reasoning, but I'm not sure if it's correct. Here it goes:
Domain X


*

*$\forall x :\phi(x)⟹\gamma(x)$

*Let $E\subseteq X⟹[\forall x\in E :\phi(x)⟹\gamma(x)]$

*Suppose I know, by some property of $E$, that $\forall x\in E :\phi(x)$, that is for every $x\in E$, $\phi(x)$ is true.

*[$\forall x\in E :\phi(x)] ⟹ \phi(x)$ (by universal instantation)

*⟹ $\gamma(x)$ (by universal instantation of 2. and by 4.)

*⟹ $\forall x\in E :\gamma(x)$ (by universal generalization)

*Therefore: [$\forall x\in E :\phi(x)⟹\gamma(x)]\wedge [\forall x\in E :\phi(x)] ⟹ \forall x\in E :\gamma(x)$


It's like I have distributed the quantifier over the implication. Is this correct?
 A: This is correct. Note that you can go a little bit further: $\forall x(\varphi(x)\implies\psi(x))$ implies $\forall x(\varphi(x))\implies\forall x(\psi(x))$. This is one direction of distributivity of $\forall$ over $\implies$.
As a cautionary note, let me point out that similar-looking principles may not hold, e.g.: it is not the case that $$[(\forall x\varphi(x))\implies (\forall x\psi(x))\quad \color{red}{\implies}\quad  \forall x(\varphi(x)\implies\psi(x))].$$ That is, distributivity doesn't go in both directions.

Note that distributivity does work both ways for $\forall$ over $\wedge$, but (again) works only one way for $\forall$ over $\vee$. Similar but dual results hold for distribution of $\exists$ over Boolean operations.
A: *

*$\forall x : \phi(x) \implies \gamma(x)$ (premise)

*$E\subset X$ (premise)

*$\forall x \in E :\phi(x) \implies \gamma(x)$ (by 2)

*$\forall x \in E : \phi(x)$ (premise)

*$\phi(x)$ (U.I, 4)

*$\phi(x) \implies \gamma(x)$ (U.I, 3)

*$\gamma(x)$ (M.P, 5, 6)

*$\forall x \in E : \gamma(x)$ (U.G, 7)

*$\forall x \in E : \phi(x)\implies \forall x \in E : \gamma(x)$ (conditional proof, 4 - 8)

*$\forall x \in E (\phi(x) \implies \gamma(x)) \land (\forall x \in E : \phi(x))\implies \forall x \in E : \gamma(x))$ 

*$\forall x \in E (\phi(x) \implies \gamma(x)) \implies [(\forall x \in E : \phi(x))\implies (\forall x \in E : \gamma(x))]$
