Theorem bj-hbald

Description: General statement that hbald proves . (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypotheses	bj-hbald.1	|- ( ph -> A. y ps )
	bj-hbald.2	|- ( ps -> ( ch -> A. x th ) )
Assertion	bj-hbald	|- ( ph -> ( A. y ch -> A. x A. y th ) )

Proof

Step	Hyp	Ref	Expression
1		bj-hbald.1	|- ( ph -> A. y ps )
2		bj-hbald.2	|- ( ps -> ( ch -> A. x th ) )
3	2	al2imi	|- ( A. y ps -> ( A. y ch -> A. y A. x th ) )
4	1 3	syl	|- ( ph -> ( A. y ch -> A. y A. x th ) )
5		ax-11	|- ( A. y A. x th -> A. x A. y th )
6	4 5	syl6	|- ( ph -> ( A. y ch -> A. x A. y th ) )