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