Theorem hbntg

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

	Ref	Expression
Assertion	hbntg	$$⊢\forall x\left(\phi \to \forall x\psi \right)\to \left(\neg \psi \to \forall x\neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		axc7	$$⊢\neg \forall x\neg \forall x\psi \to \psi$$
2	1	con1i	$$⊢\neg \psi \to \forall x\neg \forall x\psi$$
3		con3	$$⊢\left(\phi \to \forall x\psi \right)\to \left(\neg \forall x\psi \to \neg \phi \right)$$
4	3	al2imi	$$⊢\forall x\left(\phi \to \forall x\psi \right)\to \left(\forall x\neg \forall x\psi \to \forall x\neg \phi \right)$$
5	2 4	syl5	$$⊢\forall x\left(\phi \to \forall x\psi \right)\to \left(\neg \psi \to \forall x\neg \phi \right)$$