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 1427 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 |
This theorem was proved from axioms: ax-ial 1427 |
This theorem is referenced by: nfa1 1434 a5i 1435 hba2 1443 hbia1 1444 19.21h 1449 19.21ht 1473 exim 1490 19.12 1555 19.38 1566 ax9o 1588 equveli 1642 nfald 1643 equs5a 1675 ax11v2 1701 equs5 1710 equs5or 1711 sb56 1765 hbsb4t 1889 hbeu1 1910 eupickbi 1982 moexexdc 1984 2eu4 1993 exists2 1997 hbra1 2354 |
Copyright terms: Public domain | W3C validator |