Theorem hbald

Description: Deduction form of bound-variable hypothesis builder hbal . (Contributed by NM, 2-Jan-2002)

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

Proof

Step	Hyp	Ref	Expression
1		hbald.1	|- ( ph -> A. y ph )
2		hbald.2	|- ( ph -> ( ps -> A. x ps ) )
3	1 2	alimdh	|- ( ph -> ( A. y ps -> A. y A. x ps ) )
4		ax-11	|- ( A. y A. x ps -> A. x A. y ps )
5	3 4	syl6	|- ( ph -> ( A. y ps -> A. x A. y ps ) )