Description: First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 ( hba1 ). (Contributed by BJ, 21-Dec-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-modal4e | |- ( E. x E. x ph -> E. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-modal4 | |- ( A. x -. ph -> A. x A. x -. ph ) |
|
| 2 | alnex | |- ( A. x -. ph <-> -. E. x ph ) |
|
| 3 | 2exnaln | |- ( E. x E. x ph <-> -. A. x A. x -. ph ) |
|
| 4 | 3 | con2bii | |- ( A. x A. x -. ph <-> -. E. x E. x ph ) |
| 5 | 1 2 4 | 3imtr3i | |- ( -. E. x ph -> -. E. x E. x ph ) |
| 6 | 5 | con4i | |- ( E. x E. x ph -> E. x ph ) |