Metamath Proof Explorer


Theorem bj-modald

Description: A short form of the axiom D of modal logic. (Contributed by BJ, 4-Apr-2021)

Ref Expression
Assertion bj-modald x ¬ φ ¬ x φ

Proof

Step Hyp Ref Expression
1 19.2 x φ x φ
2 df-ex x φ ¬ x ¬ φ
3 1 2 sylib x φ ¬ x ¬ φ
4 3 con2i x ¬ φ ¬ x φ