Theorem modal-b

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

Conclusion

\( \vdash \varphi \rightarrow \forall x \, \neg \forall x \, \neg \varphi \)

Proof

axc7

con4i _