Description: Lemma for bj-vtoclg1f1 (an instance of this lemma is a version of bj-vtoclg1f1 where x and y are identified). (Contributed by BJ, 30-Apr-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-exlimmpi.nf | |- F/ x ps |
|
bj-exlimmpi.maj | |- ( ch -> ( ph -> ps ) ) |
||
bj-exlimmpi.min | |- ph |
||
Assertion | bj-exlimmpi | |- ( E. x ch -> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-exlimmpi.nf | |- F/ x ps |
|
2 | bj-exlimmpi.maj | |- ( ch -> ( ph -> ps ) ) |
|
3 | bj-exlimmpi.min | |- ph |
|
4 | 3 2 | mpi | |- ( ch -> ps ) |
5 | 1 4 | exlimi | |- ( E. x ch -> ps ) |