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 | |- ( A. x ph -> A. x A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-modalbe | |- ( A. x ph -> A. x E. x A. x ph ) |
|
| 2 | hbe1a | |- ( E. x A. x ph -> A. x ph ) |
|
| 3 | 1 2 | sylg | |- ( A. x ph -> A. x A. x ph ) |