Theorem alsbid

Description: Deduction form of alsbii . (Contributed by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Hypotheses	alsbid.1	|- F/ x ph
	alsbid.2	|- ( ph -> ( ps <-> th ) )
	alsbid.3	|- ( ph -> ( ch <-> ta ) )
Assertion	alsbid	|- ( ph -> ( AE x ( ps -> ch ) <-> AE x ( th -> ta ) ) )

Proof

Step	Hyp	Ref	Expression
1		alsbid.1	|- F/ x ph
2		alsbid.2	|- ( ph -> ( ps <-> th ) )
3		alsbid.3	|- ( ph -> ( ch <-> ta ) )
4	2 3	imbi12d	|- ( ph -> ( ( ps -> ch ) <-> ( th -> ta ) ) )
5	1 4	albid	|- ( ph -> ( A. x ( ps -> ch ) <-> A. x ( th -> ta ) ) )
6	1 2	exbid	|- ( ph -> ( E. x ps <-> E. x th ) )
7	5 6	anbi12d	|- ( ph -> ( ( A. x ( ps -> ch ) /\ E. x ps ) <-> ( A. x ( th -> ta ) /\ E. x th ) ) )
8		df-als	|- ( AE x ( ps -> ch ) <-> ( A. x ( ps -> ch ) /\ E. x ps ) )
9		df-als	|- ( AE x ( th -> ta ) <-> ( A. x ( th -> ta ) /\ E. x th ) )
10	7 8 9	3bitr4g	|- ( ph -> ( AE x ( ps -> ch ) <-> AE x ( th -> ta ) ) )