Theorem hba1-o

Description: The setvar x is not free in A. x ph . Example in Appendix in Megill p. 450 (p. 19 of the preprint). Also Lemma 22 of Monk2 p. 114. (Contributed by NM, 24-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hba1-o	$$⊢\forall x\phi \to \forall x\forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-c5	$$⊢\forall x\neg \forall x\phi \to \neg \forall x\phi$$
2	1	con2i	$$⊢\forall x\phi \to \neg \forall x\neg \forall x\phi$$
3		ax10fromc7	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\neg \forall x\neg \forall x\phi$$
4		ax10fromc7	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$
5	4	con1i	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\phi$$
6	5	alimi	$$⊢\forall x\neg \forall x\neg \forall x\phi \to \forall x\forall x\phi$$
7	2 3 6	3syl	$$⊢\forall x\phi \to \forall x\forall x\phi$$