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.)