Description: Alternate proof of aleximi from exim , which is sometimes used as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-aleximiALT.1 | |- ( ph -> ( ps -> ch ) ) |
|
Assertion | bj-aleximiALT | |- ( A. x ph -> ( E. x ps -> E. x ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-aleximiALT.1 | |- ( ph -> ( ps -> ch ) ) |
|
2 | 1 | alimi | |- ( A. x ph -> A. x ( ps -> ch ) ) |
3 | bj-eximALT | |- ( A. x ( ps -> ch ) -> ( E. x ps -> E. x ch ) ) |
|
4 | 2 3 | syl | |- ( A. x ph -> ( E. x ps -> E. x ch ) ) |