Theorem pm10.251

Description: Theorem *10.251 in WhiteheadRussell p. 149. (Contributed by Andrew Salmon, 17-Jun-2011)

	Ref	Expression
Assertion	pm10.251	$$⊢\forall x\neg \phi \to \neg \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
2		19.2	$$⊢\forall x\phi \to \exists x\phi$$
3	2	con3i	$$⊢\neg \exists x\phi \to \neg \forall x\phi$$
4	1 3	sylbi	$$⊢\forall x\neg \phi \to \neg \forall x\phi$$