Metamath Proof Explorer

Theorem bj-eximcom

Description: A commuted form of exim which is sometimes posited as an axiom in instuitionistic modal logic. (Contributed by BJ, 9-Dec-2023)

Ref Expression
Assertion bj-eximcom 
|- ( E. x ( ph -> ps ) -> ( A. x ph -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 pm2.27 
 |-  ( ph -> ( ( ph -> ps ) -> ps ) )
2 1 aleximi 
 |-  ( A. x ph -> ( E. x ( ph -> ps ) -> E. x ps ) )
3 2 com12 
 |-  ( E. x ( ph -> ps ) -> ( A. x ph -> E. x ps ) )