Type  Label  Description 
Statement 

Theorem  19.23 1801 
Theorem 19.23 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)
(Revised by Mario Carneiro, 24Sep2016.)



Theorem  19.23h 1802 
Theorem 19.23 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)
(Revised by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf
Lammen, 1Jan2018.)



Theorem  exlimi 1803 
Inference from Theorem 19.23 of [Margaris] p.
90. (Contributed by Mario
Carneiro, 24Sep2016.)



Theorem  exlimih 1804 
Inference from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.) (Proof shortened by Andrew Salmon, 13May2011.) (Proof
shortened by Wolf Lammen, 1Jan2018.)



Theorem  exlimihOLD 1805 
Obsolete proof of exlimih 1804 as of 1Jan2018. (Contributed by NM,
5Aug1993.) (Proof shortened by Andrew Salmon, 13May2011.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  exlimd 1806 
Deduction from Theorem 19.23 of [Margaris] p.
90. (Contributed by Mario
Carneiro, 24Sep2016.)



Theorem  exlimdh 1807 
Deduction from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
28Jan1997.)



Theorem  nfimd 1808 
If in a context is
not free in and
, it is not free
in . (Contributed by Mario Carneiro, 24Sep2016.)
(Proof shortened by Wolf Lammen, 30Dec2017.)



Theorem  nfimdOLD 1809 
Obsolete proof of nfimd 1808 as of 29Dec2017. (Contributed by Mario
Carneiro, 24Sep2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  hbim1 1810 
A closed form of hbim 1817. (Contributed by NM, 5Aug1993.)



Theorem  nfim1 1811 
A closed form of nfim 1813. (Contributed by NM, 5Aug1993.) (Revised
by
Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf Lammen,
2Jan2018.)



Theorem  nfim1OLD 1812 
A closed form of nfim 1813. (Contributed by NM, 5Aug1993.) (Revised
by
Mario Carneiro, 24Sep2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfim 1813 
If is not free in
and , it is not free in
. (Contributed by Mario Carneiro, 11Aug2016.)
(Proof shortened by Wolf Lammen, 2Jan2018.)



Theorem  nfimOLD 1814 
If is not free in
and , it is not free in
. (Contributed by Mario Carneiro, 11Aug2016.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  hbimd 1815 
Deduction form of boundvariable hypothesis builder hbim 1817.
(Contributed by NM, 1Jan2002.) (Proof shortened by Wolf Lammen,
3Jan2018.)



Theorem  hbimdOLD 1816 
Obsolete proof of hbimd 1815 as of 16Dec2017. (Contributed by NM,
1Jan2002.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  hbim 1817 
If is not free in
and , it is not free in
. (Contributed by NM, 5Aug1993.) (Proof shortened
by O'Cat, 3Mar2008.) (Proof shortened by Wolf Lammen, 1Jan2018.)



Theorem  hbimOLD 1818 
Obsolete proof of hbim 1817 as of 1Jan2018. (Contributed by NM,
5Aug1993.) (Proof shortened by O'Cat, 3Mar2008.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  19.23tOLD 1819 
Obsolete proof of 19.23t 1800 as of 1Jan2018. (Contributed by NM,
7Nov2005.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  19.23hOLD 1820 
Obsolete proof of 19.23h 1802 as of 1Jan2018. (Contributed by NM,
5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  spimehOLD 1821* 
Obsolete proof of spimeh 1667 as of 10Dec2017. (Contributed by NM,
7Aug1994.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfand 1822 
If in a context is
not free in and
, it is not free
in .
(Contributed by Mario Carneiro, 7Oct2016.)



Theorem  nf3and 1823 
Deduction form of boundvariable hypothesis builder nf3an 1827.
(Contributed by NM, 17Feb2013.) (Revised by Mario Carneiro,
16Oct2016.)



Theorem  nfan 1824 
If is not free in
and , it is not free in
.
(Contributed by Mario Carneiro, 11Aug2016.)
(Proof shortned by Wolf Lammen, 2Jan2018.)



Theorem  nfnan 1825 
If is not free in
and , then it is not free in
. (Contributed by Scott Fenton, 2Jan2018.)



Theorem  nfanOLD 1826 
Obsolete proof of nfan 1824 as of 2Jan2018. (Contributed by Mario
Carneiro, 11Aug2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nf3an 1827 
If is not free in
, , and , it is not free in
. (Contributed by Mario
Carneiro,
11Aug2016.)



Theorem  hban 1828 
If is not free in
and , it is not free in
.
(Contributed by NM, 5Aug1993.) (Proof shortened
by Wolf Lammen, 2Jan2018.)



Theorem  hbanOLD 1829 
Obsolete proof of hban 1828 as of 2Jan2018. (Contributed by NM,
5Aug1993.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  hb3an 1830 
If is not free in
, , and , it is not free in
. (Contributed by NM,
14Sep2003.) (Proof
shortened by Wolf Lammen, 2Jan2018.)



Theorem  hb3anOLD 1831 
Obsolete proof of hb3an 1830 as of 2Jan2018. (Contributed by NM,
14Sep2003.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfbid 1832 
If in a context is
not free in and
, it is not free
in . (Contributed by Mario Carneiro,
24Sep2016.)
(Proof shortened by Wolf Lammen, 29Dec2017.)



Theorem  nfbidOLD 1833 
Obsolete proof of nfbid 1832 as of 29Dec2017. (Contributed by Mario
Carneiro, 24Sep2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfbi 1834 
If is not free in
and , it is not free in
. (Contributed by Mario Carneiro,
11Aug2016.)
(Proof shortened by Wolf Lammen, 2Jan2018.)



Theorem  nfbiOLD 1835 
If is not free in
and , it is not free in
. (Contributed by Mario Carneiro,
11Aug2016.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  nfor 1836 
If is not free in
and , it is not free in
.
(Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nf3or 1837 
If is not free in
, , and , it is not free in
. (Contributed by Mario
Carneiro,
11Aug2016.)



Theorem  equsalhw 1838* 
Weaker version of equsalh 1961 (requiring distinct variables) without using
ax12 1925. (Contributed by NM, 29Nov2015.) (Proof
shortened by Wolf
Lammen, 28Dec2017.)



Theorem  equsalhwOLD 1839* 
Obsolete proof of equsalhw 1838 as of 28Dec2017. (Contributed by NM,
29Nov2015.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  19.21hOLD 1840 
Obsolete proof of 19.21h 1797 as of 1Jan2018. (Contributed by NM,
1Aug2017.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  hbex 1841 
If is not free in
, it is not free
in .
(Contributed by NM, 5Aug1993.)



Theorem  nfal 1842 
If is not free in
, it is not free
in .
(Contributed by Mario Carneiro, 11Aug2016.)



Theorem  nfex 1843 
If is not free in
, it is not free
in .
(Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf
Lammen, 30Dec2017.)



Theorem  nfexOLD 1844 
Obsolete proof of nfex 1843 as of 30Dec2017. (Contributed by Mario
Carneiro, 11Aug2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfnf 1845 
If is not free in
, it is not free
in .
(Contributed by Mario Carneiro, 11Aug2016.) (Proof shortened by Wolf
Lammen, 30Dec2017.)



Theorem  nfnfOLD 1846 
Obsolete proof of nfnf 1845 as of 30Dec2017. (Contributed by Mario
Carneiro, 11Aug2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  19.12 1847 
Theorem 19.12 of [Margaris] p. 89. Assuming
the converse is a mistake
sometimes made by beginners! But sometimes the converse does hold, as in
19.12vv 1898 and r19.12sn 3789. (Contributed by NM, 5Aug1993.) (Proof
shortened by Wolf Lammen, 3Jan2018.)



Theorem  19.12OLD 1848 
Obsolete proof of 19.12 1847 as of 3Jan2018. (Contributed by NM,
5Aug1993.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  dvelimhw 1849* 
Proof of dvelimh 1964 without using ax12 1925 but with additional distinct
variable conditions. (Contributed by Andrew Salmon, 21Jul2011.)
(Revised by NM, 1Aug2017.)



Theorem  cbv3hv 1850* 
Lemma for ax10 1944. Similar to cbv3h 1983. Requires distinct variables
but avoids ax12 1925. (Contributed by NM, 25Jul2015.) (Proof
shortened by Wolf Lammen, 29Dec2017.)



Theorem  cbv3hvOLD 1851* 
Obsolete proof of cbv3hv 1850 as of 29Dec2017. (Contributed by NM,
25Jul2015.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfald 1852 
If is not free in
, it is not free
in .
(Contributed by Mario Carneiro, 24Sep2016.) (Proof shortened by Wolf
Lammen, 6Jan2018.)



Theorem  nfaldOLD 1853 
Obsolete proof of nfald 1852 as of 6Jan2018. (Contributed by Mario
Carneiro, 24Sep2016.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  nfexd 1854 
If is not free in
, it is not free
in .
(Contributed by Mario Carneiro, 24Sep2016.)



Theorem  nfa2 1855 
Lemma 24 of [Monk2] p. 114. (Contributed by
Mario Carneiro,
24Sep2016.)



Theorem  nfia1 1856 
Lemma 23 of [Monk2] p. 114. (Contributed by
Mario Carneiro,
24Sep2016.)



Theorem  19.9tOLD 1857 
Obsolete proof of 19.9t 1779 as of 30Dec2017. (Contributed by NM,
5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.)
(Proof modification is discouraged.)(New usage is discouraged.)



Theorem  excomimOLD 1858 
Obsolete proof of excomim 1742 as of 8Jan2018. (Contributed by NM,
5Aug1993.) (Revised by Mario Carneiro, 24Sep2016.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  excomOLD 1859 
Obsolete proof of excom 1741 as of 8Jan2018. (Contributed by NM,
5Aug1993.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  19.16 1860 
Theorem 19.16 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.17 1861 
Theorem 19.17 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.19 1862 
Theorem 19.19 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.21tOLD 1863 
Obsolete proof of 19.21t 1795 as of 30Dec2017. (Contributed by NM,
27May1997.) (Revised by Mario Carneiro, 24Sep2016.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  19.212 1864 
Theorem 19.21 of [Margaris] p. 90 but with 2
quantifiers. (Contributed
by NM, 4Feb2005.)



Theorem  19.21bbi 1865 
Inference removing double quantifier. (Contributed by NM,
20Apr1994.)



Theorem  nf2 1866 
An alternative definition of dfnf 1545, which does not involve nested
quantifiers on the same variable. (Contributed by Mario Carneiro,
24Sep2016.)



Theorem  nf3 1867 
An alternative definition of dfnf 1545. (Contributed by Mario Carneiro,
24Sep2016.)



Theorem  nf4 1868 
Variable is
effectively not free in iff
is always true
or always false. (Contributed by Mario Carneiro, 24Sep2016.)



Theorem  19.27 1869 
Theorem 19.27 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.28 1870 
Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.36 1871 
Theorem 19.36 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.36i 1872 
Inference from Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  19.37 1873 
Theorem 19.37 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.38OLD 1874 
Obsolete proof of 19.38 as of 2Jan2018. (Contributed by NM,
5Aug1993.) (Proof modification is discouraged.)
(New usage is discouraged.)



Theorem  19.32 1875 
Theorem 19.32 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)
(Revised by Mario Carneiro, 24Sep2016.)



Theorem  19.31 1876 
Theorem 19.31 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.44 1877 
Theorem 19.44 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.45 1878 
Theorem 19.45 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)



Theorem  19.41 1879 
Theorem 19.41 of [Margaris] p. 90.
(Contributed by NM, 5Aug1993.)
(Proof shortened by Andrew Salmon, 25May2011.)



Theorem  19.42 1880 
Theorem 19.42 of [Margaris] p. 90.
(Contributed by NM, 18Aug1993.)



Theorem  nfan1 1881 
A closed form of nfan 1824. (Contributed by Mario Carneiro,
3Oct2016.)



Theorem  exan 1882 
Place a conjunct in the scope of an existential quantifier.
(Contributed by NM, 18Aug1993.) (Proof shortened by Andrew Salmon,
25May2011.)



Theorem  hbnd 1883 
Deduction form of boundvariable hypothesis builder hbn 1776.
(Contributed by NM, 3Jan2002.)



Theorem  aaan 1884 
Rearrange universal quantifiers. (Contributed by NM, 12Aug1993.)



Theorem  eeor 1885 
Rearrange existential quantifiers. (Contributed by NM, 8Aug1994.)



Theorem  qexmid 1886 
Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111,
Computability and Logic. (Contributed by NM, 10Dec2000.)



Theorem  equs5a 1887 
A property related to substitution that unlike equs5 1996 doesn't require a
distinctor antecedent. (Contributed by NM, 2Feb2007.)



Theorem  equs5e 1888 
A property related to substitution that unlike equs5 1996 doesn't require a
distinctor antecedent. (Contributed by NM, 2Feb2007.)



Theorem  exlimdd 1889 
Existential elimination rule of natural deduction. (Contributed by
Mario Carneiro, 9Feb2017.)



Theorem  19.21v 1890* 
Special case of Theorem 19.21 of [Margaris] p.
90. Notational
convention: We sometimes suffix with "v" the label of a
theorem
eliminating a hypothesis such as in 19.21 1796 via the use of
distinct variable conditions combined with nfv 1619.
Conversely, we
sometimes suffix with "f" the label of a theorem introducing
such a
hypothesis to eliminate the need for the distinct variable condition;
e.g. euf 2210 derived from dfeu 2208. The "f" stands for "not free
in"
which is less restrictive than "does not occur in."
(Contributed by NM,
5Aug1993.)



Theorem  19.23v 1891* 
Special case of Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
28Jun1998.)



Theorem  19.23vv 1892* 
Theorem 19.23 of [Margaris] p. 90 extended to
two variables.
(Contributed by NM, 10Aug2004.)



Theorem  pm11.53 1893* 
Theorem *11.53 in [WhiteheadRussell]
p. 164. (Contributed by Andrew
Salmon, 24May2011.)



Theorem  19.27v 1894* 
Theorem 19.27 of [Margaris] p. 90.
(Contributed by NM, 3Jun2004.)



Theorem  19.28v 1895* 
Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 25Mar2004.)



Theorem  19.36v 1896* 
Special case of Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
18Aug1993.)



Theorem  19.36aiv 1897* 
Inference from Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  19.12vv 1898* 
Special case of 19.12 1847 where its converse holds. (Contributed by
NM,
18Jul2001.) (Revised by Andrew Salmon, 11Jul2011.)



Theorem  19.37v 1899* 
Special case of Theorem 19.37 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)



Theorem  19.37aiv 1900* 
Inference from Theorem 19.37 of [Margaris] p.
90. (Contributed by NM,
5Aug1993.)

