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 ) |
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 ) |