Theorem hba1 1503

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

Syntax hints:   → wi 4  ∀wal 1312

This theorem was proved from axioms:  ax-ial 1497

This theorem is referenced by:  nfa1  1504  a5i  1505  hba2  1513  hbia1  1514  19.21h  1519  19.21ht  1543  exim  1561  19.12  1626  19.38  1637  ax9o  1659  equveli  1715  nfald  1716  equs5a  1748  ax11v2  1774  equs5  1783  equs5or  1784  sb56  1839  hbsb4t  1964  hbeu1  1985  eupickbi  2057  moexexdc  2059  2eu4  2068  exists2  2072  hbra1  2439