Theorem hba1 1593

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

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-ial 1587

This theorem is referenced by:  nfa1  1594  a5i  1596  hba2  1604  hbia1  1605  19.21h  1610  19.21ht  1634  exim  1652  19.12  1717  19.38  1728  ax9o  1750  equveli  1812  nfald  1813  equs5a  1847  ax11v2  1873  equs5  1882  equs5or  1883  sb56  1940  hbsb4t  2073  hbeu1  2096  eupickbi  2169  moexexdc  2171  2eu4  2180  exists2  2184  hbra1  2580