Theorem hbntal

Description: A closed form of hbn . hbnt is another closed form of hbn . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hba1	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \forall x\forall x\left(\phi \to \forall x\phi \right)$$
2		axc7	$$⊢\neg \forall x\neg \forall x\phi \to \phi$$
3	2	con1i	$$⊢\neg \phi \to \forall x\neg \forall x\phi$$
4		con3	$$⊢\left(\phi \to \forall x\phi \right)\to \left(\neg \forall x\phi \to \neg \phi \right)$$
5	4	al2imi	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \left(\forall x\neg \forall x\phi \to \forall x\neg \phi \right)$$
6	3 5	syl5	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \left(\neg \phi \to \forall x\neg \phi \right)$$
7	6	alimi	$$⊢\forall x\forall x\left(\phi \to \forall x\phi \right)\to \forall x\left(\neg \phi \to \forall x\neg \phi \right)$$
8	1 7	syl	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \forall x\left(\neg \phi \to \forall x\neg \phi \right)$$