Theorem bj-19.41t 34103

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

Assertion

Ref	Expression
bj-19.41t	⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))

Proof of Theorem bj-19.41t

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∃wex 1780  Ⅎ'wnnf 34055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-bj-nnf 34056

This theorem is referenced by: (None)