![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > hba1 | GIF version |
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.) |
Ref | Expression |
---|---|
hba1 | ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ial 1534 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 |
This theorem was proved from axioms: ax-ial 1534 |
This theorem is referenced by: nfa1 1541 a5i 1543 hba2 1551 hbia1 1552 19.21h 1557 19.21ht 1581 exim 1599 19.12 1665 19.38 1676 ax9o 1698 equveli 1759 nfald 1760 equs5a 1794 ax11v2 1820 equs5 1829 equs5or 1830 sb56 1885 hbsb4t 2013 hbeu1 2036 eupickbi 2108 moexexdc 2110 2eu4 2119 exists2 2123 hbra1 2507 |
Copyright terms: Public domain | W3C validator |