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 1521 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 |
This theorem was proved from axioms: ax-ial 1521 |
This theorem is referenced by: nfa1 1528 a5i 1530 hba2 1538 hbia1 1539 19.21h 1544 19.21ht 1568 exim 1586 19.12 1652 19.38 1663 ax9o 1685 equveli 1746 nfald 1747 equs5a 1781 ax11v2 1807 equs5 1816 equs5or 1817 sb56 1872 hbsb4t 2000 hbeu1 2023 eupickbi 2095 moexexdc 2097 2eu4 2106 exists2 2110 hbra1 2494 |
Copyright terms: Public domain | W3C validator |