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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modalbe | |
|
2 | hbe1a | |
|
3 | 1 2 | sylg | |