Theorem hba1 1554

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-ial 1548

This theorem is referenced by:  nfa1  1555  a5i  1557  hba2  1565  hbia1  1566  19.21h  1571  19.21ht  1595  exim  1613  19.12  1679  19.38  1690  ax9o  1712  equveli  1773  nfald  1774  equs5a  1808  ax11v2  1834  equs5  1843  equs5or  1844  sb56  1900  hbsb4t  2032  hbeu1  2055  eupickbi  2127  moexexdc  2129  2eu4  2138  exists2  2142  hbra1  2527