Theorem hba1 1564

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-ial 1558

This theorem is referenced by:  nfa1  1565  a5i  1567  hba2  1575  hbia1  1576  19.21h  1581  19.21ht  1605  exim  1623  19.12  1689  19.38  1700  ax9o  1722  equveli  1783  nfald  1784  equs5a  1818  ax11v2  1844  equs5  1853  equs5or  1854  sb56  1910  hbsb4t  2042  hbeu1  2065  eupickbi  2137  moexexdc  2139  2eu4  2148  exists2  2152  hbra1  2537