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	⊢ ( 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		axc7	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 )
2	1	con4i	⊢ ( 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 ¬ 𝜑 )