Theorem bj-sblem

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

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

Proof

Step	Hyp	Ref	Expression
1		pm5.74	|- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
2	1	albii	|- ( A. x ( ph -> ( ps <-> ch ) ) <-> A. x ( ( ph -> ps ) <-> ( ph -> ch ) ) )
3		albi	|- ( A. x ( ( ph -> ps ) <-> ( ph -> ch ) ) -> ( A. x ( ph -> ps ) <-> A. x ( ph -> ch ) ) )
4	2 3	sylbi	|- ( A. x ( ph -> ( ps <-> ch ) ) -> ( A. x ( ph -> ps ) <-> A. x ( ph -> ch ) ) )
5		19.23v	|- ( A. x ( ph -> ch ) <-> ( E. x ph -> ch ) )
6	4 5	bitrdi	|- ( A. x ( ph -> ( ps <-> ch ) ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ch ) ) )