Theorem bj-19.41al

Description: Special case of 19.41 proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-19.41al	$$⊢\exists x\left(\phi \wedge \forall x\psi \right)\leftrightarrow \left(\exists x\phi \wedge \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.40	$$⊢\exists x\left(\phi \wedge \forall x\psi \right)\to \left(\exists x\phi \wedge \exists x\forall x\psi \right)$$
2		hbe1a	$$⊢\exists x\forall x\psi \to \forall x\psi$$
3	2	anim2i	$$⊢\left(\exists x\phi \wedge \exists x\forall x\psi \right)\to \left(\exists x\phi \wedge \forall x\psi \right)$$
4	1 3	syl	$$⊢\exists x\left(\phi \wedge \forall x\psi \right)\to \left(\exists x\phi \wedge \forall x\psi \right)$$
5		hba1	$$⊢\forall x\psi \to \forall x\forall x\psi$$
6	5	anim2i	$$⊢\left(\exists x\phi \wedge \forall x\psi \right)\to \left(\exists x\phi \wedge \forall x\forall x\psi \right)$$
7		19.29r	$$⊢\left(\exists x\phi \wedge \forall x\forall x\psi \right)\to \exists x\left(\phi \wedge \forall x\psi \right)$$
8	6 7	syl	$$⊢\left(\exists x\phi \wedge \forall x\psi \right)\to \exists x\left(\phi \wedge \forall x\psi \right)$$
9	4 8	impbii	$$⊢\exists x\left(\phi \wedge \forall x\psi \right)\leftrightarrow \left(\exists x\phi \wedge \forall x\psi \right)$$