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 ( ∃ 𝑥 𝜒𝜓 )

Proof

Step Hyp Ref Expression
1 bj-exlimvmpi.maj ( 𝜒 → ( 𝜑𝜓 ) )
2 bj-exlimvmpi.min 𝜑
3 2 1 mpi ( 𝜒𝜓 )
4 3 exlimiv ( ∃ 𝑥 𝜒𝜓 )