Theorem hba1 1528

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

Syntax hints:   → wi 4  ∀wal 1341

This theorem was proved from axioms:  ax-ial 1522

This theorem is referenced by:  nfa1  1529  a5i  1531  hba2  1539  hbia1  1540  19.21h  1545  19.21ht  1569  exim  1587  19.12  1653  19.38  1664  ax9o  1686  equveli  1747  nfald  1748  equs5a  1782  ax11v2  1808  equs5  1817  equs5or  1818  sb56  1873  hbsb4t  2001  hbeu1  2024  eupickbi  2096  moexexdc  2098  2eu4  2107  exists2  2111  hbra1  2496