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

Metamath Proof Explorer

Theorem bj-cbveximt

Description: A lemma in closed form used to prove bj-cbvex 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-cbveximt ⊢ ∀ x ∃ y χ → ∀ x ∀ y χ → φ → ψ → ∀ x φ → ∀ y φ → ∃ x ∃ y ψ → ∃ y ψ → ∃ x φ → ∃ y ψ

Proof

Step Hyp Ref Expression
1 bj-exalim ⊢ ∀ y χ → φ → ψ → ∃ y χ → ∀ y φ → ∃ y ψ
2 1 alimi ⊢ ∀ x ∀ y χ → φ → ψ → ∀ x ∃ y χ → ∀ y φ → ∃ y ψ
3 bj-alexim ⊢ ∀ x ∃ y χ → ∀ y φ → ∃ y ψ → ∀ x ∃ y χ → ∃ x ∀ y φ → ∃ x ∃ y ψ
4 2 3 syl ⊢ ∀ x ∀ y χ → φ → ψ → ∀ x ∃ y χ → ∃ x ∀ y φ → ∃ x ∃ y ψ
5 exim ⊢ ∀ x φ → ∀ y φ → ∃ x φ → ∃ x ∀ y φ
6 imim2 ⊢ ∃ x ∀ y φ → ∃ x ∃ y ψ → ∃ x φ → ∃ x ∀ y φ → ∃ x φ → ∃ x ∃ y ψ
7 imim1 ⊢ ∃ x φ → ∃ x ∃ y ψ → ∃ x ∃ y ψ → ∃ y ψ → ∃ x φ → ∃ y ψ
8 5 6 7 syl56 ⊢ ∃ x ∀ y φ → ∃ x ∃ y ψ → ∀ x φ → ∀ y φ → ∃ x ∃ y ψ → ∃ y ψ → ∃ x φ → ∃ y ψ
9 4 8 syl6com ⊢ ∀ x ∃ y χ → ∀ x ∀ y χ → φ → ψ → ∀ x φ → ∀ y φ → ∃ x ∃ y ψ → ∃ y ψ → ∃ x φ → ∃ y ψ