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 1282 | . 2 wff ∀𝑥𝜑 |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
This axiom is referenced by: a17d 1460 nfv 1461 exlimiv 1529 equid 1629 ax16 1734 dvelimfALT2 1738 exlimdv 1740 ax11a2 1742 albidv 1745 exbidv 1746 ax11v 1748 ax11ev 1749 ax16i 1779 ax16ALT 1780 equvin 1784 19.9v 1792 19.21v 1794 alrimiv 1795 alrimdv 1797 alimdv 1800 eximdv 1801 19.23v 1804 pm11.53 1816 19.27v 1820 19.28v 1821 19.41v 1823 19.42v 1827 cbvalv 1835 cbvexv 1836 cbvexdh 1842 nexdv 1852 cleljust 1854 sbhb 1857 hbsbv 1858 sbco2v 1862 nfsb 1863 equsb3lem 1865 equsb3 1866 sbn 1867 sbim 1868 sbor 1869 sban 1870 sbco3 1889 nfsbt 1891 elsb3 1893 elsb4 1894 sb9 1896 sbcom2v2 1903 sbcom2 1904 dfsb7 1908 sbid2v 1913 sbelx 1914 sbal 1917 sbal1 1919 sbex 1921 exsb 1925 dvelimALT 1927 dvelim 1934 dvelimor 1935 dveel1 1937 dveel2 1938 euf 1946 sb8euh 1964 euorv 1968 euex 1971 euanv 1998 mo4f 2001 moim 2005 moimv 2007 moanim 2015 mopick 2019 2eu4 2034 cleqh 2178 abeq2 2187 mpteq12 3861 bj-ex 10573 bj-inex 10698 |
Copyright terms: Public domain | W3C validator |