Theorem bj-cbvalimt 36640

Description: A lemma in closed form used to prove bj-cbval 36650 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1877 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-cbvalimt	⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓)))))

Proof of Theorem bj-cbvalimt

Step	Hyp	Ref	Expression
1		exim 1834	. . 3 ⊢ (∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∃𝑥𝜒 → ∃𝑥(𝜑 → 𝜓)))
2	1	al2imi 1815	. 2 ⊢ (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → (∀𝑦∃𝑥𝜒 → ∀𝑦∃𝑥(𝜑 → 𝜓)))
3		pm2.27 42	. . . . . 6 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
4	3	aleximi 1832	. . . . 5 ⊢ (∀𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → ∃𝑥𝜓))
5	4	com12 32	. . . 4 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
6	5	alimi 1811	. . 3 ⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → ∀𝑦(∀𝑥𝜑 → ∃𝑥𝜓))
7		alim 1810	. . 3 ⊢ (∀𝑦(∀𝑥𝜑 → ∃𝑥𝜓) → (∀𝑦∀𝑥𝜑 → ∀𝑦∃𝑥𝜓))
8		alim 1810	. . . . 5 ⊢ (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑦∃𝑥𝜓 → ∀𝑦𝜓))
9		imim1 83	. . . . 5 ⊢ ((∀𝑦∀𝑥𝜑 → ∀𝑦∃𝑥𝜓) → ((∀𝑦∃𝑥𝜓 → ∀𝑦𝜓) → (∀𝑦∀𝑥𝜑 → ∀𝑦𝜓)))
10		imim2 58	. . . . 5 ⊢ ((∀𝑦∀𝑥𝜑 → ∀𝑦𝜓) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
11	8, 9, 10	syl56 36	. . . 4 ⊢ ((∀𝑦∀𝑥𝜑 → ∀𝑦∃𝑥𝜓) → (∀𝑦(∃𝑥𝜓 → 𝜓) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))))
12	11	com23 86	. . 3 ⊢ ((∀𝑦∀𝑥𝜑 → ∀𝑦∃𝑥𝜓) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))
13	6, 7, 12	3syl 18	. 2 ⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))
14	2, 13	syl6com 37	1 ⊢ (∀𝑦∃𝑥𝜒 → (∀𝑦∀𝑥(𝜒 → (𝜑 → 𝜓)) → ((∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) → (∀𝑦(∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓)))))

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  bj-cbvalim  36646