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 
|- ( A. x -. ph -> -. A. x ph )

Proof

Step Hyp Ref Expression
1 19.2 
 |-  ( A. x ph -> E. x ph )
2 df-ex 
 |-  ( E. x ph <-> -. A. x -. ph )
3 1 2 sylib 
 |-  ( A. x ph -> -. A. x -. ph )
4 3 con2i 
 |-  ( A. x -. ph -> -. A. x ph )