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 ⊢ ∀ y ∃ x χ → ∀ y ∀ x χ → φ → ψ → ∀ x φ → ∀ y ∀ x φ → ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y ψ

Proof

Step Hyp Ref Expression
1 exim ⊢ ∀ x χ → φ → ψ → ∃ x χ → ∃ x φ → ψ
2 1 al2imi ⊢ ∀ y ∀ x χ → φ → ψ → ∀ y ∃ x χ → ∀ y ∃ x φ → ψ
3 pm2.27 ⊢ φ → φ → ψ → ψ
4 3 aleximi ⊢ ∀ x φ → ∃ x φ → ψ → ∃ x ψ
5 4 com12 ⊢ ∃ x φ → ψ → ∀ x φ → ∃ x ψ
6 5 alimi ⊢ ∀ y ∃ x φ → ψ → ∀ y ∀ x φ → ∃ x ψ
7 alim ⊢ ∀ y ∀ x φ → ∃ x ψ → ∀ y ∀ x φ → ∀ y ∃ x ψ
8 alim ⊢ ∀ y ∃ x ψ → ψ → ∀ y ∃ x ψ → ∀ y ψ
9 imim1 ⊢ ∀ y ∀ x φ → ∀ y ∃ x ψ → ∀ y ∃ x ψ → ∀ y ψ → ∀ y ∀ x φ → ∀ y ψ
10 imim2 ⊢ ∀ y ∀ x φ → ∀ y ψ → ∀ x φ → ∀ y ∀ x φ → ∀ x φ → ∀ y ψ
11 8 9 10 syl56 ⊢ ∀ y ∀ x φ → ∀ y ∃ x ψ → ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y ∀ x φ → ∀ x φ → ∀ y ψ
12 11 com23 ⊢ ∀ y ∀ x φ → ∀ y ∃ x ψ → ∀ x φ → ∀ y ∀ x φ → ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y ψ
13 6 7 12 3syl ⊢ ∀ y ∃ x φ → ψ → ∀ x φ → ∀ y ∀ x φ → ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y ψ
14 2 13 syl6com ⊢ ∀ y ∃ x χ → ∀ y ∀ x χ → φ → ψ → ∀ x φ → ∀ y ∀ x φ → ∀ y ∃ x ψ → ψ → ∀ x φ → ∀ y ψ