![]() |
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 1294 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1472 nfv 1473 exlimiv 1541 equid 1641 ax16 1748 dvelimfALT2 1752 exlimdv 1754 ax11a2 1756 albidv 1759 exbidv 1760 ax11v 1762 ax11ev 1763 ax16i 1793 ax16ALT 1794 equvin 1798 19.9v 1806 19.21v 1808 alrimiv 1809 alrimdv 1811 alimdv 1814 eximdv 1815 19.23v 1818 pm11.53 1830 19.27v 1834 19.28v 1835 19.41v 1837 19.42v 1841 cbvalv 1849 cbvexv 1850 cbvexdh 1856 nexdv 1866 cleljust 1868 sbhb 1871 hbsbv 1872 sbco2v 1876 nfsb 1877 equsb3lem 1879 equsb3 1880 sbn 1881 sbim 1882 sbor 1883 sban 1884 sbco3 1903 nfsbt 1905 elsb3 1907 elsb4 1908 sb9 1910 sbcom2v2 1917 sbcom2 1918 dfsb7 1922 sbid2v 1927 sbelx 1928 sbal 1931 sbal1 1933 sbex 1935 exsb 1939 dvelimALT 1941 dvelim 1948 dvelimor 1949 dveel1 1951 dveel2 1952 euf 1960 sb8euh 1978 euorv 1982 euex 1985 euanv 2012 mo4f 2015 moim 2019 moimv 2021 moanim 2029 mopick 2033 2eu4 2048 cleqh 2194 abeq2 2203 mpteq12 3943 bj-ex 12375 bj-inex 12510 |
Copyright terms: Public domain | W3C validator |