Theorem bj-sblem2

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		19.23v	|- ( A. x ( ph -> ch ) <-> ( E. x ph -> ch ) )
2		ax-2	|- ( ( ph -> ( ch -> ps ) ) -> ( ( ph -> ch ) -> ( ph -> ps ) ) )
3	2	al2imi	|- ( A. x ( ph -> ( ch -> ps ) ) -> ( A. x ( ph -> ch ) -> A. x ( ph -> ps ) ) )
4	1 3	syl5bir	|- ( A. x ( ph -> ( ch -> ps ) ) -> ( ( E. x ph -> ch ) -> A. x ( ph -> ps ) ) )