Theorem hba1 1551

Description: 𝑥 is not free in ∀𝑥𝜑. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
hba1	⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)

Proof of Theorem hba1

Step	Hyp	Ref	Expression
1		ax-ial 1545	1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-ial 1545

This theorem is referenced by:  nfa1  1552  a5i  1554  hba2  1562  hbia1  1563  19.21h  1568  19.21ht  1592  exim  1610  19.12  1676  19.38  1687  ax9o  1709  equveli  1770  nfald  1771  equs5a  1805  ax11v2  1831  equs5  1840  equs5or  1841  sb56  1897  hbsb4t  2029  hbeu1  2052  eupickbi  2124  moexexdc  2126  2eu4  2135  exists2  2139  hbra1  2524