Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-17 | GIF version |
Description: Axiom to quantify a
variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ax-17 | ⊢ (𝜑 → ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | 1, 2 | wal 1329 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1507 nfv 1508 exlimiv 1577 equid 1677 ax16 1785 dvelimfALT2 1789 exlimdv 1791 ax11a2 1793 albidv 1796 exbidv 1797 ax11v 1799 ax11ev 1800 ax16i 1830 ax16ALT 1831 equvin 1835 19.9v 1843 19.21v 1845 alrimiv 1846 alrimdv 1848 alimdv 1851 eximdv 1852 19.23v 1855 pm11.53 1867 19.27v 1871 19.28v 1872 19.41v 1874 19.42v 1878 cbvalv 1889 cbvexv 1890 cbvexdh 1898 nexdv 1908 cleljust 1910 sbhb 1913 hbsbv 1914 sbco2vh 1918 nfsb 1919 equsb3lem 1923 equsb3 1924 sbn 1925 sbim 1926 sbor 1927 sban 1928 sbco3 1947 nfsbt 1949 elsb3 1951 elsb4 1952 sb9 1954 sbcom2v2 1961 sbcom2 1962 dfsb7 1966 sbid2v 1971 sbelx 1972 sbal 1975 sbal1 1977 sbex 1979 exsb 1983 dvelimALT 1985 dvelim 1992 dvelimor 1993 dveel1 1995 dveel2 1996 euf 2004 sb8euh 2022 euorv 2026 euex 2029 euanv 2056 mo4f 2059 moim 2063 moimv 2065 moanim 2073 mopick 2077 2eu4 2092 cleqh 2239 abeq2 2248 mpteq12 4011 bj-ex 12969 bj-inex 13105 |
Copyright terms: Public domain | W3C validator |