Theorem bj-hbal

Description: More general instance of hbal . (Contributed by BJ, 4-Apr-2026)

	Ref	Expression
Hypothesis	bj-hbal.1	|- ( ph -> A. x ps )
Assertion	bj-hbal	|- ( A. y ph -> A. x A. y ps )

Proof

Step	Hyp	Ref	Expression
1		bj-hbal.1	|- ( ph -> A. x ps )
2		bj-hbalt	|- ( A. y ( ph -> A. x ps ) -> ( A. y ph -> A. x A. y ps ) )
3	2 1	mpg	|- ( A. y ph -> A. x A. y ps )