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