This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-cbvalimt

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

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

Proof

Step Hyp Ref Expression
1 exim ⊢ ( ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 𝜒 → ∃ 𝑥 ( 𝜑 → 𝜓 ) ) )
2 1 al2imi ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ∀ 𝑦 ∃ 𝑥 𝜒 → ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) ) )
3 pm2.27 ⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
4 3 aleximi ⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ∃ 𝑥 𝜓 ) )
5 4 com12 ⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
6 5 alimi ⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑦 ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
7 alim ⊢ ( ∀ 𝑦 ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) → ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) )
8 alim ⊢ ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑦 ∃ 𝑥 𝜓 → ∀ 𝑦 𝜓 ) )
9 imim1 ⊢ ( ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) → ( ( ∀ 𝑦 ∃ 𝑥 𝜓 → ∀ 𝑦 𝜓 ) → ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) )
10 imim2 ⊢ ( ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) )
11 8 9 10 syl56 ⊢ ( ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) )
12 11 com23 ⊢ ( ( ∀ 𝑦 ∀ 𝑥 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) )
13 6 7 12 3syl ⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) )
14 2 13 syl6com ⊢ ( ∀ 𝑦 ∃ 𝑥 𝜒 → ( ∀ 𝑦 ∀ 𝑥 ( 𝜒 → ( 𝜑 → 𝜓 ) ) → ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ( ∃ 𝑥 𝜓 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 ) ) ) ) )