Theorem alsbii

Description: Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Hypotheses	alsbii.1	|- ( ph <-> ch )
	alsbii.2	|- ( ps <-> th )
Assertion	alsbii	|- ( AE x ( ph -> ps ) <-> AE x ( ch -> th ) )

Proof

Step	Hyp	Ref	Expression
1		alsbii.1	|- ( ph <-> ch )
2		alsbii.2	|- ( ps <-> th )
3	1 2	imbi12i	|- ( ( ph -> ps ) <-> ( ch -> th ) )
4	3	albii	|- ( A. x ( ph -> ps ) <-> A. x ( ch -> th ) )
5	1	exbii	|- ( E. x ph <-> E. x ch )
6	4 5	anbi12i	|- ( ( A. x ( ph -> ps ) /\ E. x ph ) <-> ( A. x ( ch -> th ) /\ E. x ch ) )
7		df-als	|- ( AE x ( ph -> ps ) <-> ( A. x ( ph -> ps ) /\ E. x ph ) )
8		df-als	|- ( AE x ( ch -> th ) <-> ( A. x ( ch -> th ) /\ E. x ch ) )
9	6 7 8	3bitr4i	|- ( AE x ( ph -> ps ) <-> AE x ( ch -> th ) )