Theorem hba1 1562

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

Syntax hints:   → wi 4  ∀wal 1370

This theorem was proved from axioms:  ax-ial 1556

This theorem is referenced by:  nfa1  1563  a5i  1565  hba2  1573  hbia1  1574  19.21h  1579  19.21ht  1603  exim  1621  19.12  1687  19.38  1698  ax9o  1720  equveli  1781  nfald  1782  equs5a  1816  ax11v2  1842  equs5  1851  equs5or  1852  sb56  1908  hbsb4t  2040  hbeu1  2063  eupickbi  2135  moexexdc  2137  2eu4  2146  exists2  2150  hbra1  2535