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 1514 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 |
This theorem was proved from axioms: ax-ial 1514 |
This theorem is referenced by: nfa1 1521 a5i 1522 hba2 1530 hbia1 1531 19.21h 1536 19.21ht 1560 exim 1578 19.12 1643 19.38 1654 ax9o 1676 equveli 1732 nfald 1733 equs5a 1766 ax11v2 1792 equs5 1801 equs5or 1802 sb56 1857 hbsb4t 1988 hbeu1 2009 eupickbi 2081 moexexdc 2083 2eu4 2092 exists2 2096 hbra1 2465 |
Copyright terms: Public domain | W3C validator |