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	⊢ ( Ⅎ' 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		exancom	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) )
2		bj-19.42t	⊢ ( Ⅎ' 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜓 ∧ 𝜑 ) ↔ ( 𝜓 ∧ ∃ 𝑥 𝜑 ) ) )
3	1 2	syl5bb	⊢ ( Ⅎ' 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ ∃ 𝑥 𝜑 ) ) )
4	3	biancomd	⊢ ( Ⅎ' 𝑥 𝜓 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ 𝜓 ) ) )