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  1807  nfald  1808  equs5a  1842  ax11v2  1868  equs5  1877  equs5or  1878  sb56  1934  hbsb4t  2066  hbeu1  2089  eupickbi  2162  moexexdc  2164  2eu4  2173  exists2  2177  hbra1  2563