Metamath Proof Explorer


Theorem bj-modal4

Description: First-order logic form of the modal axiom (4). See hba1 . This is the standard proof of the implication in modal logic (B5 => 4). Its dual statement is bj-modal4e . (Contributed by BJ, 12-Aug-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-modal4 xφxxφ

Proof

Step Hyp Ref Expression
1 bj-modalbe xφxxxφ
2 hbe1a xxφxφ
3 1 2 sylg xφxxφ