Theorem pm11.61

Description: Theorem *11.61 in WhiteheadRussell p. 166. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm11.61	$$⊢\exists y\forall x\left(\phi \to \psi \right)\to \forall x\left(\phi \to \exists y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.12	$$⊢\exists y\forall x\left(\phi \to \psi \right)\to \forall x\exists y\left(\phi \to \psi \right)$$
2		19.37v	$$⊢\exists y\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \exists y\psi \right)$$
3	2	biimpi	$$⊢\exists y\left(\phi \to \psi \right)\to \left(\phi \to \exists y\psi \right)$$
4	3	alimi	$$⊢\forall x\exists y\left(\phi \to \psi \right)\to \forall x\left(\phi \to \exists y\psi \right)$$
5	1 4	syl	$$⊢\exists y\forall x\left(\phi \to \psi \right)\to \forall x\left(\phi \to \exists y\psi \right)$$