Theorem bj-19.41t 37710

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

Assertion

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

Proof of Theorem bj-19.41t

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1811  Ⅎ'wnnf 37670

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-bj-nnf 37671

This theorem is used by: (None)