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

Proof

Step Hyp Ref Expression
1 modal-b 
 |-  ( ph -> A. x -. A. x -. ph )
2 df-ex 
 |-  ( E. x ph <-> -. A. x -. ph )
3 2 biimpri 
 |-  ( -. A. x -. ph -> E. x ph )
4 1 3 sylg 
 |-  ( ph -> A. x E. x ph )