Metamath Proof Explorer
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 |
⊢ ( ∃ 𝑥 𝜒 → 𝜓 ) |