Metamath Proof Explorer


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 φ x x φ

Proof

Step Hyp Ref Expression
1 modal-b φ x ¬ x ¬ φ
2 df-ex x φ ¬ x ¬ φ
3 2 biimpri ¬ x ¬ φ x φ
4 1 3 sylg φ x x φ