This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hbal

Description: If x is not free in ph , it is not free in A. y ph . (Contributed by NM, 12-Mar-1993)

		Ref	Expression
	Hypothesis	hbal.1	$⊢ φ \to \forall x φ$
	Assertion	hbal	$⊢ \forall y φ \to \forall x \forall y φ$

Step	Hyp	Ref	Expression
1		hbal.1	$⊢ φ \to \forall x φ$
2	1	alimi	$⊢ \forall y φ \to \forall y \forall x φ$
3		ax-11	$⊢ \forall y \forall x φ \to \forall x \forall y φ$
4	2 3	syl	$⊢ \forall y φ \to \forall x \forall y φ$