Theorem bj-19.41t 37419

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

Assertion

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

Proof of Theorem bj-19.41t

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400  ∃wex 1808  Ⅎ'wnnf 37379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-bj-nnf 37380

This theorem is used by: (None)