Theorem hbalw

Description: Weak version of hbal . Uses only Tarski's FOL axiom schemes. Unlike hbal , this theorem requires that x and y be distinct, i.e. not be bundled. (Contributed by NM, 19-Apr-2017)

	Ref	Expression
Hypotheses	hbalw.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
	hbalw.2	$$⊢\phi \to \forall x\phi$$
Assertion	hbalw	$$⊢\forall y\phi \to \forall x\forall y\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbalw.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
2		hbalw.2	$$⊢\phi \to \forall x\phi$$
3	2	alimi	$$⊢\forall y\phi \to \forall y\forall x\phi$$
4	1	alcomiw	$$⊢\forall y\forall x\phi \to \forall x\forall y\phi$$
5	3 4	syl	$$⊢\forall y\phi \to \forall x\forall y\phi$$