Theorem bj-19.41t 34883

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

Assertion

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

Proof of Theorem bj-19.41t

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃wex 1783  Ⅎ'wnnf 34832

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-bj-nnf 34833

This theorem is referenced by: (None)