Description: Dual statement of sylg (the final "e" in the label stands for "existential (version of sylg )". Variant of exlimih . (Contributed by BJ, 25-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-sylge.nf | |- ( E. x ph -> ps ) |
|
| bj-sylge.maj | |- ( ch -> ph ) |
||
| Assertion | bj-sylge | |- ( E. x ch -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-sylge.nf | |- ( E. x ph -> ps ) |
|
| 2 | bj-sylge.maj | |- ( ch -> ph ) |
|
| 3 | 2 | eximi | |- ( E. x ch -> E. x ph ) |
| 4 | 3 1 | syl | |- ( E. x ch -> ps ) |