Theorem pm10.57

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

	Ref	Expression
Assertion	pm10.57	$$⊢\forall x\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\forall x\left(\phi \to \psi \right)\vee \exists x\left(\phi \wedge \chi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		alnex	$$⊢\forall x\neg \left(\phi \wedge \chi \right)\leftrightarrow \neg \exists x\left(\phi \wedge \chi \right)$$
2		imnan	$$⊢\left(\phi \to \neg \chi \right)\leftrightarrow \neg \left(\phi \wedge \chi \right)$$
3		pm2.53	$$⊢\left(\psi \vee \chi \right)\to \left(\neg \psi \to \chi \right)$$
4	3	con1d	$$⊢\left(\psi \vee \chi \right)\to \left(\neg \chi \to \psi \right)$$
5	4	imim3i	$$⊢\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\left(\phi \to \neg \chi \right)\to \left(\phi \to \psi \right)\right)$$
6	2 5	syl5bir	$$⊢\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\neg \left(\phi \wedge \chi \right)\to \left(\phi \to \psi \right)\right)$$
7	6	al2imi	$$⊢\forall x\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\forall x\neg \left(\phi \wedge \chi \right)\to \forall x\left(\phi \to \psi \right)\right)$$
8	1 7	syl5bir	$$⊢\forall x\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\neg \exists x\left(\phi \wedge \chi \right)\to \forall x\left(\phi \to \psi \right)\right)$$
9	8	con1d	$$⊢\forall x\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\neg \forall x\left(\phi \to \psi \right)\to \exists x\left(\phi \wedge \chi \right)\right)$$
10	9	orrd	$$⊢\forall x\left(\phi \to \left(\psi \vee \chi \right)\right)\to \left(\forall x\left(\phi \to \psi \right)\vee \exists x\left(\phi \wedge \chi \right)\right)$$