Metamath Proof Explorer


Theorem bj-exlimmpbir

Description: Lemma for theorems of the vtoclg family. (Contributed by BJ, 3-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-exlimmpbir.nf x φ
bj-exlimmpbir.maj χ φ ψ
bj-exlimmpbir.min ψ
Assertion bj-exlimmpbir x χ φ

Proof

Step Hyp Ref Expression
1 bj-exlimmpbir.nf x φ
2 bj-exlimmpbir.maj χ φ ψ
3 bj-exlimmpbir.min ψ
4 3 2 mpbiri χ φ
5 1 4 exlimi x χ φ