Theorem hba1 1586

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

Syntax hints:   → wi 4  ∀wal 1393

This theorem was proved from axioms:  ax-ial 1580

This theorem is referenced by:  nfa1  1587  a5i  1589  hba2  1597  hbia1  1598  19.21h  1603  19.21ht  1627  exim  1645  19.12  1711  19.38  1722  ax9o  1744  equveli  1805  nfald  1806  equs5a  1840  ax11v2  1866  equs5  1875  equs5or  1876  sb56  1932  hbsb4t  2064  hbeu1  2087  eupickbi  2160  moexexdc  2162  2eu4  2171  exists2  2175  hbra1  2560