Theorem bj-spimt2

Description: A step in the proof of spimt . (Contributed by BJ, 2-May-2019)

	Ref	Expression
Assertion	bj-spimt2	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-alequex	|- ( A. x ( x = y -> ( ph -> ps ) ) -> E. x ( ph -> ps ) )
2		19.35	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
3	1 2	sylib	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ph -> E. x ps ) )
4	3	imim1d	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( ( E. x ps -> ps ) -> ( A. x ph -> ps ) ) )