Metamath Proof Explorer


Theorem bj-modal4e

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 x x φ x φ

Proof

Step Hyp Ref Expression
1 bj-modal4 x ¬ φ x x ¬ φ
2 alnex x ¬ φ ¬ x φ
3 2exnaln x x φ ¬ x x ¬ φ
4 3 con2bii x x ¬ φ ¬ x x φ
5 1 2 4 3imtr3i ¬ x φ ¬ x x φ
6 5 con4i x x φ x φ