Theorem modal-b

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

	Ref	Expression
Assertion	modal-b	$$⊢\phi \to \forall x\neg \forall x\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		axc7	$$⊢\neg \forall x\neg \forall x\neg \phi \to \neg \phi$$
2	1	con4i	$$⊢\phi \to \forall x\neg \forall x\neg \phi$$