Description: An equality-free general instance of one half of a precise form of bj-cbvex . (Contributed by BJ, 12-Mar-2023) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | bj-cbvalimi.maj | |- ( ch -> ( ph -> ps ) ) |
|
bj-cbveximi.denote | |- A. x E. y ch |
||
Assertion | bj-cbveximi | |- ( E. x ph -> E. y ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-cbvalimi.maj | |- ( ch -> ( ph -> ps ) ) |
|
2 | bj-cbveximi.denote | |- A. x E. y ch |
|
3 | 1 | gen2 | |- A. x A. y ( ch -> ( ph -> ps ) ) |
4 | bj-cbvexim | |- ( A. x E. y ch -> ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( E. x ph -> E. y ps ) ) ) |
|
5 | 2 3 4 | mp2 | |- ( E. x ph -> E. y ps ) |