Metamath Proof Explorer


Theorem bj-cbvalim

Description: A lemma used to prove bj-cbval in a weak axiomatization. (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-cbvalim y x χ y x χ φ ψ x φ y ψ

Proof

Step Hyp Ref Expression
1 ax5e x ψ ψ
2 1 ax-gen y x ψ ψ
3 ax-5 x φ y x φ
4 bj-cbvalimt y x χ y x χ φ ψ x φ y x φ y x ψ ψ x φ y ψ
5 4 com3l y x χ φ ψ x φ y x φ y x χ y x ψ ψ x φ y ψ
6 5 com14 y x ψ ψ x φ y x φ y x χ y x χ φ ψ x φ y ψ
7 2 3 6 mp2 y x χ y x χ φ ψ x φ y ψ