Theorem bj-sblem1

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

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

Proof

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