HomeHome New Foundations Explorer
Theorem List (p. 19 of 64)
< Previous  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

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.)
xψ       (x(φψ) ↔ (xφψ))
 
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.)
(ψxψ)       (x(φψ) ↔ (xφψ))
 
Theoremexlimi 1803 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
xψ    &   (φψ)       (xφψ)
 
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.)
(ψxψ)    &   (φψ)       (xφψ)
 
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.) (New usage is discouraged.)
(ψxψ)    &   (φψ)       (xφψ)
 
Theoremexlimd 1806 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
xφ    &   xχ    &   (φ → (ψχ))       (φ → (xψχ))
 
Theoremexlimdh 1807 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
(φxφ)    &   (χxχ)    &   (φ → (ψχ))       (φ → (xψχ))
 
Theoremnfimd 1808 If in a context x 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.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψχ))
 
TheoremnfimdOLD 1809 Obsolete proof of nfimd 1808 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψχ))
 
Theoremhbim1 1810 A closed form of hbim 1817. (Contributed by NM, 5-Aug-1993.)
(φxφ)    &   (φ → (ψxψ))       ((φψ) → x(φψ))
 
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.)
xφ    &   (φ → Ⅎxψ)       x(φψ)
 
Theoremnfim1OLD 1812 A closed form of nfim 1813. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.)
xφ    &   (φ → Ⅎxψ)       x(φψ)
 
Theoremnfim 1813 If x 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.)
xφ    &   xψ       x(φψ)
 
TheoremnfimOLD 1814 If x is not free in φ and ψ, it is not free in (φψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
xφ    &   xψ       x(φψ)
 
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.)
(φxφ)    &   (φ → (ψxψ))    &   (φ → (χxχ))       (φ → ((ψχ) → x(ψχ)))
 
TheoremhbimdOLD 1816 Obsolete proof of hbimd 1815 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.)
(φxφ)    &   (φ → (ψxψ))    &   (φ → (χxχ))       (φ → ((ψχ) → x(ψχ)))
 
Theoremhbim 1817 If x 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.)
(φxφ)    &   (ψxψ)       ((φψ) → x(φψ))
 
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.) (New usage is discouraged.)
(φxφ)    &   (ψxψ)       ((φψ) → x(φψ))
 
Theorem19.23tOLD 1819 Obsolete proof of 19.23t 1800 as of 1-Jan-2018. (Contributed by NM, 7-Nov-2005.) (New usage is discouraged.)
(Ⅎxψ → (x(φψ) ↔ (xφψ)))
 
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.) (New usage is discouraged.)
(ψxψ)       (x(φψ) ↔ (xφψ))
 
TheoremspimehOLD 1821* Obsolete proof of spimeh 1667 as of 10-Dec-2017. (Contributed by NM, 7-Aug-1994.) (New usage is discouraged.)
(φxφ)    &   (x = z → (φψ))       (φxψ)
 
Theoremnfand 1822 If in a context x is not free in ψ and χ, it is not free in (ψ χ). (Contributed by Mario Carneiro, 7-Oct-2016.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψ χ))
 
Theoremnf3and 1823 Deduction form of bound-variable hypothesis builder nf3an 1827. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)    &   (φ → Ⅎxθ)       (φ → Ⅎx(ψ χ θ))
 
Theoremnfan 1824 If x 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.)
xφ    &   xψ       x(φ ψ)
 
Theoremnfnan 1825 If x is not free in φ and ψ, then it is not free in (φ ψ). (Contributed by Scott Fenton, 2-Jan-2018.)
xφ    &   xψ       x(φ ψ)
 
TheoremnfanOLD 1826 Obsolete proof of nfan 1824 as of 2-Jan-2018. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
xφ    &   xψ       x(φ ψ)
 
Theoremnf3an 1827 If x is not free in φ, ψ, and χ, it is not free in (φ ψ χ). (Contributed by Mario Carneiro, 11-Aug-2016.)
xφ    &   xψ    &   xχ       x(φ ψ χ)
 
Theoremhban 1828 If x is not free in φ and ψ, it is not free in (φ ψ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
(φxφ)    &   (ψxψ)       ((φ ψ) → x(φ ψ))
 
TheoremhbanOLD 1829 Obsolete proof of hban 1828 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
(φxφ)    &   (ψxψ)       ((φ ψ) → x(φ ψ))
 
Theoremhb3an 1830 If x is not free in φ, ψ, and χ, it is not free in (φ ψ χ). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
(φxφ)    &   (ψxψ)    &   (χxχ)       ((φ ψ χ) → x(φ ψ χ))
 
Theoremhb3anOLD 1831 Obsolete proof of hb3an 1830 as of 2-Jan-2018. (Contributed by NM, 14-Sep-2003.) (New usage is discouraged.)
(φxφ)    &   (ψxψ)    &   (χxχ)       ((φ ψ χ) → x(φ ψ χ))
 
Theoremnfbid 1832 If in a context x 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.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψχ))
 
TheoremnfbidOLD 1833 Obsolete proof of nfbid 1832 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.)
(φ → Ⅎxψ)    &   (φ → Ⅎxχ)       (φ → Ⅎx(ψχ))
 
Theoremnfbi 1834 If x 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.)
xφ    &   xψ       x(φψ)
 
TheoremnfbiOLD 1835 If x is not free in φ and ψ, it is not free in (φψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
xφ    &   xψ       x(φψ)
 
Theoremnfor 1836 If x is not free in φ and ψ, it is not free in (φ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.)
xφ    &   xψ       x(φ ψ)
 
Theoremnf3or 1837 If x is not free in φ, ψ, and χ, it is not free in (φ ψ χ). (Contributed by Mario Carneiro, 11-Aug-2016.)
xφ    &   xψ    &   xχ       x(φ ψ χ)
 
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.)
(ψxψ)    &   (x = y → (φψ))       (x(x = yφ) ↔ ψ)
 
TheoremequsalhwOLD 1839* Obsolete proof of equsalhw 1838 as of 28-Dec-2017. (Contributed by NM, 29-Nov-2015.) (New usage is discouraged.)
(ψxψ)    &   (x = y → (φψ))       (x(x = yφ) ↔ ψ)
 
Theorem19.21hOLD 1840 Obsolete proof of 19.21h 1797 as of 1-Jan-2018. (Contributed by NM, 1-Aug-2017.) (New usage is discouraged.)
(φxφ)       (x(φψ) ↔ (φxψ))
 
Theoremhbex 1841 If x is not free in φ, it is not free in yφ. (Contributed by NM, 5-Aug-1993.)
(φxφ)       (yφxyφ)
 
Theoremnfal 1842 If x is not free in φ, it is not free in yφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
xφ       xyφ
 
Theoremnfex 1843 If x is not free in φ, it is not free in yφ. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
xφ       xyφ
 
TheoremnfexOLD 1844 Obsolete proof of nfex 1843 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
xφ       xyφ
 
Theoremnfnf 1845 If x is not free in φ, it is not free in yφ. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
xφ       xyφ
 
TheoremnfnfOLD 1846 Obsolete proof of nfnf 1845 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
xφ       xyφ
 
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.)
(xyφyxφ)
 
Theorem19.12OLD 1848 Obsolete proof of 19.12 1847 as of 3-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
(xyφyxφ)
 
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.)
(φxφ)    &   (ψzψ)    &   (z = y → (φψ))    &   x x = y → (y = zx y = z))       x x = y → (ψxψ))
 
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.)
(φyφ)    &   (ψxψ)    &   (x = y → (φψ))       (xφyψ)
 
Theoremcbv3hvOLD 1851* Obsolete proof of cbv3hv 1850 as of 29-Dec-2017. (Contributed by NM, 25-Jul-2015.) (New usage is discouraged.)
(φyφ)    &   (ψxψ)    &   (x = y → (φψ))       (xφyψ)
 
Theoremnfald 1852 If x is not free in φ, it is not free in yφ. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
yφ    &   (φ → Ⅎxψ)       (φ → Ⅎxyψ)
 
TheoremnfaldOLD 1853 Obsolete proof of nfald 1852 as of 6-Jan-2018. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.)
yφ    &   (φ → Ⅎxψ)       (φ → Ⅎxyψ)
 
Theoremnfexd 1854 If x is not free in φ, it is not free in yφ. (Contributed by Mario Carneiro, 24-Sep-2016.)
yφ    &   (φ → Ⅎxψ)       (φ → Ⅎxyψ)
 
Theoremnfa2 1855 Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
xyxφ
 
Theoremnfia1 1856 Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
x(xφxψ)
 
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.) (New usage is discouraged.)
(Ⅎxφ → (xφφ))
 
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.) (New usage is discouraged.)
(xyφyxφ)
 
TheoremexcomOLD 1859 Obsolete proof of excom 1741 as of 8-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
(xyφyxφ)
 
Theorem19.16 1860 Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xφ       (x(φψ) → (φxψ))
 
Theorem19.17 1861 Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ       (x(φψ) → (xφψ))
 
Theorem19.19 1862 Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xφ       (x(φψ) → (φxψ))
 
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.) (New usage is discouraged.)
(Ⅎxφ → (x(φψ) ↔ (φxψ)))
 
Theorem19.21-2 1864 Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
xφ    &   yφ       (xy(φψ) ↔ (φxyψ))
 
Theorem19.21bbi 1865 Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
(φxyψ)       (φψ)
 
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.)
(Ⅎxφ ↔ (xφxφ))
 
Theoremnf3 1867 An alternative definition of df-nf 1545. (Contributed by Mario Carneiro, 24-Sep-2016.)
(Ⅎxφx(xφφ))
 
Theoremnf4 1868 Variable x is effectively not free in φ iff φ is always true or always false. (Contributed by Mario Carneiro, 24-Sep-2016.)
(Ⅎxφ ↔ (xφ x ¬ φ))
 
Theorem19.27 1869 Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ       (x(φ ψ) ↔ (xφ ψ))
 
Theorem19.28 1870 Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xφ       (x(φ ψ) ↔ (φ xψ))
 
Theorem19.36 1871 Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ       (x(φψ) ↔ (xφψ))
 
Theorem19.36i 1872 Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ    &   x(φψ)       (xφψ)
 
Theorem19.37 1873 Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xφ       (x(φψ) ↔ (φxψ))
 
Theorem19.38OLD 1874 Obsolete proof of 19.38 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
((xφxψ) → x(φψ))
 
Theorem19.32 1875 Theorem 19.32 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
xφ       (x(φ ψ) ↔ (φ xψ))
 
Theorem19.31 1876 Theorem 19.31 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ       (x(φ ψ) ↔ (xφ ψ))
 
Theorem19.44 1877 Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xψ       (x(φ ψ) ↔ (xφ ψ))
 
Theorem19.45 1878 Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
xφ       (x(φ ψ) ↔ (φ xψ))
 
Theorem19.41 1879 Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
xψ       (x(φ ψ) ↔ (xφ ψ))
 
Theorem19.42 1880 Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
xφ       (x(φ ψ) ↔ (φ xψ))
 
Theoremnfan1 1881 A closed form of nfan 1824. (Contributed by Mario Carneiro, 3-Oct-2016.)
xφ    &   (φ → Ⅎxψ)       x(φ ψ)
 
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.)
(xφ ψ)       x(φ ψ)
 
Theoremhbnd 1883 Deduction form of bound-variable hypothesis builder hbn 1776. (Contributed by NM, 3-Jan-2002.)
(φxφ)    &   (φ → (ψxψ))       (φ → (¬ ψx ¬ ψ))
 
Theoremaaan 1884 Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
yφ    &   xψ       (xy(φ ψ) ↔ (xφ yψ))
 
Theoremeeor 1885 Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
yφ    &   xψ       (xy(φ ψ) ↔ (xφ yψ))
 
Theoremqexmid 1886 Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic. (Contributed by NM, 10-Dec-2000.)
x(φxφ)
 
Theoremequs5a 1887 A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
(x(x = y yφ) → x(x = yφ))
 
Theoremequs5e 1888 A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
(x(x = y φ) → x(x = yyφ))
 
Theoremexlimdd 1889 Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
xφ    &   xχ    &   (φxψ)    &   ((φ ψ) → χ)       (φχ)
 
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 xφ 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.)
(x(φψ) ↔ (φxψ))
 
Theorem19.23v 1891* Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
(x(φψ) ↔ (xφψ))
 
Theorem19.23vv 1892* Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
(xy(φψ) ↔ (xyφψ))
 
Theorempm11.53 1893* Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
(xy(φψ) ↔ (xφyψ))
 
Theorem19.27v 1894* Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
(x(φ ψ) ↔ (xφ ψ))
 
Theorem19.28v 1895* Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
(x(φ ψ) ↔ (φ xψ))
 
Theorem19.36v 1896* Special case of Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
(x(φψ) ↔ (xφψ))
 
Theorem19.36aiv 1897* Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
x(φψ)       (xφψ)
 
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.)
(xy(φψ) ↔ yx(φψ))
 
Theorem19.37v 1899* Special case of Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
(x(φψ) ↔ (φxψ))
 
Theorem19.37aiv 1900* Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
x(φψ)       (φxψ)
    < 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-6308
  Copyright terms: Public domain < Previous  Next >