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	$$⊢\exists x\exists x\phi \to \exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		bj-modal4	$$⊢\forall x\neg \phi \to \forall x\forall x\neg \phi$$
2		alnex	$$⊢\forall x\neg \phi \leftrightarrow \neg \exists x\phi$$
3		2exnaln	$$⊢\exists x\exists x\phi \leftrightarrow \neg \forall x\forall x\neg \phi$$
4	3	con2bii	$$⊢\forall x\forall x\neg \phi \leftrightarrow \neg \exists x\exists x\phi$$
5	1 2 4	3imtr3i	$$⊢\neg \exists x\phi \to \neg \exists x\exists x\phi$$
6	5	con4i	$$⊢\exists x\exists x\phi \to \exists x\phi$$