HomeHome New Foundations Explorer
Theorem List (p. 19 of 64)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 1801-1900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem19.23 1801 Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

 F/   =>   
 
Theorem19.23h 1802 Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
   =>   
 
Theoremexlimi 1803 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

 F/   &       =>   
 
Theoremexlimih 1804 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
   &       =>   
 
TheoremexlimihOLD 1805 Obsolete proof of exlimih 1804 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       =>   
 
Theoremexlimd 1806 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

 F/   &     F/   &       =>   
 
Theoremexlimdh 1807 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
   &       &       =>   
 
Theoremnfimd 1808 If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
 F/   &     F/   =>     F/
 
TheoremnfimdOLD 1809 Obsolete proof of nfimd 1808 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
 F/   &     F/   =>     F/
 
Theoremhbim1 1810 A closed form of hbim 1817. (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theoremnfim1 1811 A closed form of nfim 1813. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

 F/   &     F/   =>    
 F/
 
Theoremnfim1OLD 1812 A closed form of nfim 1813. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   &     F/   =>    
 F/
 
Theoremnfim 1813 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

 F/   &     F/   =>     F/
 
TheoremnfimOLD 1814 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   &     F/   =>     F/
 
Theoremhbimd 1815 Deduction form of bound-variable hypothesis builder hbim 1817. (Contributed by NM, 1-Jan-2002.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
   &       &       =>   
 
TheoremhbimdOLD 1816 Obsolete proof of hbimd 1815 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       &       =>   
 
Theoremhbim 1817 If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
   &       =>   
 
TheoremhbimOLD 1818 Obsolete proof of hbim 1817 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       =>   
 
Theorem19.23tOLD 1819 Obsolete proof of 19.23t 1800 as of 1-Jan-2018. (Contributed by NM, 7-Nov-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
 F/
 
Theorem19.23hOLD 1820 Obsolete proof of 19.23h 1802 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
   =>   
 
TheoremspimehOLD 1821* Obsolete proof of spimeh 1667 as of 10-Dec-2017. (Contributed by NM, 7-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       =>   
 
Theoremnfand 1822 If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.)
 F/   &     F/   =>     F/
 
Theoremnf3and 1823 Deduction form of bound-variable hypothesis builder nf3an 1827. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
 F/   &     F/   &     F/   =>     F/
 
Theoremnfan 1824 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortned by Wolf Lammen, 2-Jan-2018.)

 F/   &     F/   =>     F/
 
Theoremnfnan 1825 If is not free in and , then it is not free in . (Contributed by Scott Fenton, 2-Jan-2018.)

 F/   &     F/   =>     F/
 
TheoremnfanOLD 1826 Obsolete proof of nfan 1824 as of 2-Jan-2018. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   &     F/   =>     F/
 
Theoremnf3an 1827 If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   &     F/   &     F/   =>    
 F/
 
Theoremhban 1828 If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
   &       =>   
 
TheoremhbanOLD 1829 Obsolete proof of hban 1828 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       =>   
 
Theoremhb3an 1830 If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
   &       &       =>   
 
Theoremhb3anOLD 1831 Obsolete proof of hb3an 1830 as of 2-Jan-2018. (Contributed by NM, 14-Sep-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       &       =>   
 
Theoremnfbid 1832 If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
 F/   &     F/   =>     F/
 
TheoremnfbidOLD 1833 Obsolete proof of nfbid 1832 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
 F/   &     F/   =>     F/
 
Theoremnfbi 1834 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

 F/   &     F/   =>     F/
 
TheoremnfbiOLD 1835 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   &     F/   =>     F/
 
Theoremnfor 1836 If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   &     F/   =>     F/
 
Theoremnf3or 1837 If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   &     F/   &     F/   =>    
 F/
 
Theoremequsalhw 1838* Weaker version of equsalh 1961 (requiring distinct variables) without using ax-12 1925. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 28-Dec-2017.)
   &       =>   
 
TheoremequsalhwOLD 1839* Obsolete proof of equsalhw 1838 as of 28-Dec-2017. (Contributed by NM, 29-Nov-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       =>   
 
Theorem19.21hOLD 1840 Obsolete proof of 19.21h 1797 as of 1-Jan-2018. (Contributed by NM, 1-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
   =>   
 
Theoremhbex 1841 If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremnfal 1842 If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   =>    
 F/
 
Theoremnfex 1843 If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

 F/   =>    
 F/
 
TheoremnfexOLD 1844 Obsolete proof of nfex 1843 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   =>    
 F/
 
Theoremnfnf 1845 If is not free in , it is not free in  F/. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

 F/   =>    
 F/ F/
 
TheoremnfnfOLD 1846 Obsolete proof of nfnf 1845 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   =>    
 F/ F/
 
Theorem19.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, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
 
Theorem19.12OLD 1848 Obsolete proof of 19.12 1847 as of 3-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
 
Theoremdvelimhw 1849* Proof of dvelimh 1964 without using ax-12 1925 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.)
   &       &       &       =>   
 
Theoremcbv3hv 1850* Lemma for ax10 1944. Similar to cbv3h 1983. Requires distinct variables but avoids ax-12 1925. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
   &       &       =>   
 
Theoremcbv3hvOLD 1851* Obsolete proof of cbv3hv 1850 as of 29-Dec-2017. (Contributed by NM, 25-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
   &       &       =>   
 
Theoremnfald 1852 If is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)

 F/   &     F/   =>     F/
 
TheoremnfaldOLD 1853 Obsolete proof of nfald 1852 as of 6-Jan-2018. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

 F/   &     F/   =>     F/
 
Theoremnfexd 1854 If is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.)

 F/   &     F/   =>     F/
 
Theoremnfa2 1855 Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)

 F/
 
Theoremnfia1 1856 Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)

 F/
 
Theorem19.9tOLD 1857 Obsolete proof of 19.9t 1779 as of 30-Dec-2017. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.)(New usage is discouraged.)
 F/
 
TheoremexcomimOLD 1858 Obsolete proof of excomim 1742 as of 8-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
 
TheoremexcomOLD 1859 Obsolete proof of excom 1741 as of 8-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
 
Theorem19.16 1860 Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.17 1861 Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.19 1862 Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.21tOLD 1863 Obsolete proof of 19.21t 1795 as of 30-Dec-2017. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
 F/
 
Theorem19.21-2 1864 Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)

 F/   &     F/   =>   
 
Theorem19.21bbi 1865 Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
   =>   
 
Theoremnf2 1866 An alternative definition of df-nf 1545, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
 F/
 
Theoremnf3 1867 An alternative definition of df-nf 1545. (Contributed by Mario Carneiro, 24-Sep-2016.)
 F/
 
Theoremnf4 1868 Variable is effectively not free in iff is always true or always false. (Contributed by Mario Carneiro, 24-Sep-2016.)
 F/
 
Theorem19.27 1869 Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.28 1870 Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.36 1871 Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.36i 1872 Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   &       =>   
 
Theorem19.37 1873 Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.38OLD 1874 Obsolete proof of 19.38 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
 
Theorem19.32 1875 Theorem 19.32 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

 F/   =>   
 
Theorem19.31 1876 Theorem 19.31 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.44 1877 Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.45 1878 Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

 F/   =>   
 
Theorem19.41 1879 Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

 F/   =>   
 
Theorem19.42 1880 Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)

 F/   =>   
 
Theoremnfan1 1881 A closed form of nfan 1824. (Contributed by Mario Carneiro, 3-Oct-2016.)

 F/   &     F/   =>    
 F/
 
Theoremexan 1882 Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theoremhbnd 1883 Deduction form of bound-variable hypothesis builder hbn 1776. (Contributed by NM, 3-Jan-2002.)
   &       =>   
 
Theoremaaan 1884 Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)

 F/   &     F/   =>   
 
Theoremeeor 1885 Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)

 F/   &     F/   =>   
 
Theoremqexmid 1886 Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic. (Contributed by NM, 10-Dec-2000.)
 
Theoremequs5a 1887 A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
 
Theoremequs5e 1888 A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
 
Theoremexlimdd 1889 Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)

 F/   &     F/   &       &       =>   
 
Theorem19.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  F/ 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 df-eu 2208. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.)
 
Theorem19.23v 1891* Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
 
Theorem19.23vv 1892* Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
 
Theorempm11.53 1893* Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
 
Theorem19.27v 1894* Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
 
Theorem19.28v 1895* Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
 
Theorem19.36v 1896* Special case of Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
 
Theorem19.36aiv 1897* Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorem19.12vv 1898* Special case of 19.12 1847 where its converse holds. (Contributed by NM, 18-Jul-2001.) (Revised by Andrew Salmon, 11-Jul-2011.)
 
Theorem19.37v 1899* Special case of Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.37aiv 1900* Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
  Copyright terms: Public domain < Previous  Next >