Metamath Proof Explorer


Theorem bj-exlimvmpi

Description: A Fol lemma ( exlimiv followed by mpi ). (Contributed by BJ, 2-Jul-2022) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 bj-exlimvmpi.maj χ φ ψ
2 bj-exlimvmpi.min φ
3 2 1 mpi χ ψ
4 3 exlimiv x χ ψ