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

Metamath Proof Explorer

Theorem hbng

Description: A more general form of hbn . (Contributed by Scott Fenton, 13-Dec-2010)

		Ref	Expression
	Hypothesis	hbg.1	$⊢ φ \to \forall x ψ$
	Assertion	hbng	$⊢ \neg ψ \to \forall x \neg φ$

Step	Hyp	Ref	Expression
1		hbg.1	$⊢ φ \to \forall x ψ$
2		hbntg	$⊢ \forall x (φ \to \forall x ψ) \to (\neg ψ \to \forall x \neg φ)$
3	2 1	mpg	$⊢ \neg ψ \to \forall x \neg φ$