Theorem 19.30

Description: Theorem 19.30 of Margaris p. 90. (Contributed by NM, 12-Mar-1993) (Proof shortened by Andrew Salmon, 25-May-2011)

	Ref	Expression
Assertion	19.30	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \exists x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exnal	$$⊢\exists x\neg \phi \leftrightarrow \neg \forall x\phi$$
2		pm2.53	$$⊢\left(\phi \vee \psi \right)\to \left(\neg \phi \to \psi \right)$$
3	2	aleximi	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\exists x\neg \phi \to \exists x\psi \right)$$
4	1 3	syl5bir	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\neg \forall x\phi \to \exists x\psi \right)$$
5	4	orrd	$$⊢\forall x\left(\phi \vee \psi \right)\to \left(\forall x\phi \vee \exists x\psi \right)$$