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 ψ