This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to \forall x \neg \forall x \neg φ$

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