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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-modal4 | ||
2 | alnex | ||
3 | 2exnaln | ||
4 | 3 | con2bii | |
5 | 1 2 4 | 3imtr3i | |
6 | 5 | con4i |