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
|- ( ch -> ( ph -> ps ) )
bj-exlimvmpi.min
|- ph
Assertion bj-exlimvmpi
|- ( E. x ch -> ps )

Proof

Step Hyp Ref Expression
1 bj-exlimvmpi.maj
 |-  ( ch -> ( ph -> ps ) )
2 bj-exlimvmpi.min
 |-  ph
3 2 1 mpi
 |-  ( ch -> ps )
4 3 exlimiv
 |-  ( E. x ch -> ps )