Theorem moexexlem 2629

Description: Factor out the proof skeleton of moexex 2641 and moexexvw 2631. (Contributed by Wolf Lammen, 2-Oct-2023.)

Hypotheses

Ref	Expression
moexexlem.1	⊢ Ⅎ𝑦𝜑
moexexlem.2	⊢ Ⅎ𝑦∃*𝑥𝜑
moexexlem.3	⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)

Assertion

Ref	Expression
moexexlem	⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Proof of Theorem moexexlem

Step	Hyp	Ref	Expression
1		nfmo1 2560	. . . 4 ⊢ Ⅎ𝑥∃*𝑥𝜑
2		nfa1 2152	. . . . 5 ⊢ Ⅎ𝑥∀𝑥∃*𝑦𝜓
3		moexexlem.3	. . . . 5 ⊢ Ⅎ𝑥∃*𝑦∃𝑥(𝜑 ∧ 𝜓)
4	2, 3	nfim 1895	. . . 4 ⊢ Ⅎ𝑥(∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
5		moexexlem.2	. . . . . 6 ⊢ Ⅎ𝑦∃*𝑥𝜑
6		moexexlem.1	. . . . . 6 ⊢ Ⅎ𝑦𝜑
7		mopick 2628	. . . . . . . 8 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓))
8	7	ex 412	. . . . . . 7 ⊢ (∃*𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → (𝜑 → 𝜓)))
9	8	com23 86	. . . . . 6 ⊢ (∃*𝑥𝜑 → (𝜑 → (∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
10	5, 6, 9	alrimd 2216	. . . . 5 ⊢ (∃*𝑥𝜑 → (𝜑 → ∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓)))
11		moim 2547	. . . . . 6 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
12	11	spsd 2188	. . . . 5 ⊢ (∀𝑦(∃𝑥(𝜑 ∧ 𝜓) → 𝜓) → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
13	10, 12	syl6 35	. . . 4 ⊢ (∃*𝑥𝜑 → (𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
14	1, 4, 13	exlimd 2219	. . 3 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))))
15	6	nfex 2328	. . . . . 6 ⊢ Ⅎ𝑦∃𝑥𝜑
16		exsimpl 1867	. . . . . 6 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
17	15, 16	exlimi 2218	. . . . 5 ⊢ (∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
18		nexmo 2544	. . . . 5 ⊢ (¬ ∃𝑦∃𝑥(𝜑 ∧ 𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
19	17, 18	nsyl5 159	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))
20	19	a1d 25	. . 3 ⊢ (¬ ∃𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
21	14, 20	pm2.61d1 180	. 2 ⊢ (∃*𝑥𝜑 → (∀𝑥∃*𝑦𝜓 → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓)))
22	21	imp 406	1 ⊢ ((∃*𝑥𝜑 ∧ ∀𝑥∃*𝑦𝜓) → ∃*𝑦∃𝑥(𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1535  ∃wex 1777  Ⅎwnf 1781  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-mo 2543

This theorem is referenced by:  moexexvw  2631  2moswapv  2632  moexex  2641