Metamath Proof Explorer


Theorem bj-cbvexim

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

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

Proof

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