Theorem bj-alexim

Description: Closed form of aleximi . Note: this proof is shorter, so aleximi could be deduced from it ( exim would have to be proved first, see bj-eximALT but its proof is shorter (currently almost a subproof of aleximi )). (Contributed by BJ, 8-Nov-2021)

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

Proof

Step	Hyp	Ref	Expression
1		alim	|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> A. x ( ps -> ch ) ) )
2		exim	|- ( A. x ( ps -> ch ) -> ( E. x ps -> E. x ch ) )
3	1 2	syl6	|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( E. x ps -> E. x ch ) ) )