Theorem hba1 1588

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

Syntax hints:   → wi 4  ∀wal 1395

This theorem was proved from axioms:  ax-ial 1582

This theorem is referenced by:  nfa1  1589  a5i  1591  hba2  1599  hbia1  1600  19.21h  1605  19.21ht  1629  exim  1647  19.12  1713  19.38  1724  ax9o  1746  equveli  1807  nfald  1808  equs5a  1842  ax11v2  1868  equs5  1877  equs5or  1878  sb56  1934  hbsb4t  2066  hbeu1  2089  eupickbi  2162  moexexdc  2164  2eu4  2173  exists2  2177  hbra1  2562