bj-19.42t

Description: Closed form of 19.42 from the same axioms as 19.42v . (Contributed by BJ, 2-Dec-2023)

		Ref	Expression
	Assertion	bj-19.42t	$⊢ Ⅎ' x φ \to (\exists x (φ \land ψ) \leftrightarrow (φ \land \exists x ψ))$

Step	Hyp	Ref	Expression
1		19.40	$⊢ \exists x (φ \land ψ) \to (\exists x φ \land \exists x ψ)$
2		bj-nnfe	$⊢ Ⅎ' x φ \to (\exists x φ \to φ)$
3	2	anim1d	$⊢ Ⅎ' x φ \to ((\exists x φ \land \exists x ψ) \to (φ \land \exists x ψ))$
4	1 3	syl5	$⊢ Ⅎ' x φ \to (\exists x (φ \land ψ) \to (φ \land \exists x ψ))$
5		bj-nnfa	$⊢ Ⅎ' x φ \to (φ \to \forall x φ)$
6	5	anim1d	$⊢ Ⅎ' x φ \to ((φ \land \exists x ψ) \to (\forall x φ \land \exists x ψ))$
7		19.29	$⊢ (\forall x φ \land \exists x ψ) \to \exists x (φ \land ψ)$
8	6 7	syl6	$⊢ Ⅎ' x φ \to ((φ \land \exists x ψ) \to \exists x (φ \land ψ))$
9	4 8	impbid	$⊢ Ⅎ' x φ \to (\exists x (φ \land ψ) \leftrightarrow (φ \land \exists x ψ))$

Metamath Proof Explorer