Theorem bj-modalbe

Description: The predicate-calculus version of the axiom (B) of modal logic. See also modal-b . (Contributed by BJ, 20-Oct-2019)

	Ref	Expression
Assertion	bj-modalbe	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		modal-b	⊢ ( 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 ¬ 𝜑 )
2		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
3	2	biimpri	⊢ ( ¬ ∀ 𝑥 ¬ 𝜑 → ∃ 𝑥 𝜑 )
4	1 3	sylg	⊢ ( 𝜑 → ∀ 𝑥 ∃ 𝑥 𝜑 )