Theorem bj-19.41t 37314

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

Assertion

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

Proof of Theorem bj-19.41t

Step	Hyp	Ref	Expression
1		exancom 1888	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
2		bj-19.42t 37313	. . 3 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜓 ∧ 𝜑) ↔ (𝜓 ∧ ∃𝑥𝜑)))
3	1, 2	bitrid 286	. 2 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜓 ∧ ∃𝑥𝜑)))
4	3	biancomd 468	1 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1806  Ⅎ'wnnf 37274

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-bj-nnf 37275

This theorem is referenced by: (None)