Theorem modal5

Description: The analogue in our predicate calculus of axiom (5) of modal logic S5. See also hbe1 . (Contributed by NM, 5-Oct-2005)

	Ref	Expression
Assertion	modal5	$$⊢\neg \forall x\neg \phi \to \forall x\neg \forall x\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		hbn1	$$⊢\neg \forall x\neg \phi \to \forall x\neg \forall x\neg \phi$$