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 1499 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 |
This theorem was proved from axioms: ax-ial 1499 |
This theorem is referenced by: nfa1 1506 a5i 1507 hba2 1515 hbia1 1516 19.21h 1521 19.21ht 1545 exim 1563 19.12 1628 19.38 1639 ax9o 1661 equveli 1717 nfald 1718 equs5a 1750 ax11v2 1776 equs5 1785 equs5or 1786 sb56 1841 hbsb4t 1966 hbeu1 1987 eupickbi 2059 moexexdc 2061 2eu4 2070 exists2 2074 hbra1 2442 |
Copyright terms: Public domain | W3C validator |