Theorem hba1 1589

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 1583	1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-ial 1583

This theorem is referenced by:  nfa1  1590  a5i  1592  hba2  1600  hbia1  1601  19.21h  1606  19.21ht  1630  exim  1648  19.12  1713  19.38  1724  ax9o  1746  equveli  1808  nfald  1809  equs5a  1843  ax11v2  1869  equs5  1878  equs5or  1879  sb56  1935  hbsb4t  2067  hbeu1  2090  eupickbi  2163  moexexdc  2165  2eu4  2174  exists2  2178  hbra1  2572