Theorem bj-19.41t

Description: Closed form of 19.41 from the same axioms as 19.41v . The same is doable with 19.27 , 19.28 , 19.31 , 19.32 , 19.44 , 19.45 . (Contributed by BJ, 2-Dec-2023)

	Ref	Expression
Assertion	bj-19.41t	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		exancom	$$⊢\exists x\left(\phi \wedge \psi \right)\leftrightarrow \exists x\left(\psi \wedge \phi \right)$$
2		bj-19.42t	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\left(\psi \wedge \phi \right)\leftrightarrow \left(\psi \wedge \exists x\phi \right)\right)$$
3	1 2	bitrid	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\left(\phi \wedge \psi \right)\leftrightarrow \left(\psi \wedge \exists x\phi \right)\right)$$
4	3	biancomd	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\phi \wedge \psi \right)\right)$$