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

Metamath Proof Explorer

Theorem hbn

Description: If x is not free in ph , it is not free in -. ph . (Contributed by NM, 10-Jan-1993) (Proof shortened by Wolf Lammen, 17-Dec-2017)

		Ref	Expression
	Hypothesis	hbn.1	$⊢ φ \to \forall x φ$
	Assertion	hbn	$⊢ \neg φ \to \forall x \neg φ$

Step	Hyp	Ref	Expression
1		hbn.1	$⊢ φ \to \forall x φ$
2		hbnt	$⊢ \forall x (φ \to \forall x φ) \to (\neg φ \to \forall x \neg φ)$
3	2 1	mpg	$⊢ \neg φ \to \forall x \neg φ$