# Proving a theorem in predicate logic without the use of metatheorems

I'm trying to prove: $$\forall x (\phi \rightarrow \psi) \rightarrow (\forall x (\phi) \rightarrow \forall x (\psi))$$ and $$\forall x \forall y (\phi) \rightarrow \forall y \forall x (\phi)$$

using the traditional axioms of predicate logic (and whatever standard theorems from propositional logic necessary):

1. $$\forall x (\phi(x)) \rightarrow \phi(y)$$
2. $$\forall x (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall x (\psi))$$

and generalization as the inference rule: $$\vdash \phi \rightarrow \space \vdash \forall x(\phi)$$

Just to be explicit I am using the following axioms for propositional logic: $$\phi \rightarrow ( \psi \rightarrow \phi )$$ $$(\phi \rightarrow (\psi \rightarrow \theta) ) \rightarrow ((\phi \rightarrow \psi)\rightarrow (\phi \rightarrow \theta))$$ $$(\lnot\phi \rightarrow \lnot \psi) \rightarrow (\psi \rightarrow \phi)$$ and modus ponens as the inference rule.

I know how to prove these propositions using the deduction theorem, but I would like to prove them without invoking it (or any other metatheorem for that matter) .

I tried but I can't use generalization to conclude $$\psi \rightarrow \space \forall x(\psi)$$ and use hypothetical syllogism (the closed form) to get to the proposition - that is:

I get $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \space \rightarrow \space (\phi \rightarrow \psi)$$ by 1. and some theorems of propositional logic, also: $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi) ) \space \rightarrow \space \phi$$ so I conclude $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \rightarrow (\phi \land (\phi \rightarrow \psi)$$ that is: $$(\forall x (\phi \rightarrow \psi) \space \land \space \forall x (\phi)) \rightarrow \psi$$

Is there a way to continue from here...or am I way off

$$(\phi \rightarrow \psi) \vdash \forall x (\phi \rightarrow \psi)$$
if x is bounded in $$\phi$$ we get $$(\phi \rightarrow \psi) \vdash ( \phi \rightarrow \forall x ( \psi) )$$ but x is bounded in the antecedent in the last line (of the post) from which the proposition follows