Theorem pm10.251

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

	Ref	Expression
Assertion	pm10.251	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
2		19.2	⊢ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜑 )
3	2	con3i	⊢ ( ¬ ∃ 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 )
4	1 3	sylbi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ ∀ 𝑥 𝜑 )