P. 19 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.23 1801	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/xps   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.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.)
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	exlimi 1803	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xps   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exlimih 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.)
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exlimihOLD 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.)
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exlimd 1806	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- F/xch   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	exlimdh 1807	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	nfimd 1808	If in a context x is not free in ps and ch, it is not free in (ps -> ch). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps -> ch))
Theorem	nfimdOLD 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.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps -> ch))
Theorem	hbim1 1810	A closed form of hbim 1817. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	nfim1 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/xph   &   |- (ph -> F/xps)   =>   |- F/x(ph -> ps)
Theorem	nfim1OLD 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/xph   &   |- (ph -> F/xps)   =>   |- F/x(ph -> ps)
Theorem	nfim 1813	If x is not free in ph and ps, it is not free in (ph -> ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph -> ps)
Theorem	nfimOLD 1814	If x is not free in ph and ps, it is not free in (ph -> ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph -> ps)
Theorem	hbimd 1815	Deduction form of bound-variable hypothesis builder hbim 1817. (Contributed by NM, 1-Jan-2002.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	hbimdOLD 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.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	hbim 1817	If x is not free in ph and ps, it is not free in (ph -> ps). (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	hbimOLD 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.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	19.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/xps -> (A.x(ph -> ps) <-> (E.xph -> ps)))
Theorem	19.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.)
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	spimehOLD 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.)
|- (ph -> A.xph)   &   |- (x = z -> (ph -> ps))   =>   |- (ph -> E.xps)
Theorem	nfand 1822	If in a context x is not free in ps and ch, it is not free in (ps /\ ch). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps /\ ch))
Theorem	nf3and 1823	Deduction form of bound-variable hypothesis builder nf3an 1827. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   &   |- (ph -> F/xth)   =>   |- (ph -> F/x(ps /\ ch /\ th))
Theorem	nfan 1824	If x is not free in ph and ps, it is not free in (ph /\ ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortned by Wolf Lammen, 2-Jan-2018.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph /\ ps)
Theorem	nfnan 1825	If x is not free in ph and ps, then it is not free in (ph -/\ ps). (Contributed by Scott Fenton, 2-Jan-2018.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph -/\ ps)
Theorem	nfanOLD 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/xph   &   |- F/xps   =>   |- F/x(ph /\ ps)
Theorem	nf3an 1827	If x is not free in ph, ps, and ch, it is not free in (ph /\ ps /\ ch). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   &   |- F/xps   &   |- F/xch   =>   |- F/x(ph /\ ps /\ ch)
Theorem	hban 1828	If x is not free in ph and ps, it is not free in (ph /\ ps). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))
Theorem	hbanOLD 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.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))
Theorem	hb3an 1830	If x is not free in ph, ps, and ch, it is not free in (ph /\ ps /\ ch). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))
Theorem	hb3anOLD 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.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))
Theorem	nfbid 1832	If in a context x is not free in ps and ch, it is not free in (ps <-> ch). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps <-> ch))
Theorem	nfbidOLD 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.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps <-> ch))
Theorem	nfbi 1834	If x is not free in ph and ps, it is not free in (ph <-> ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph <-> ps)
Theorem	nfbiOLD 1835	If x is not free in ph and ps, it is not free in (ph <-> ps). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph <-> ps)
Theorem	nfor 1836	If x is not free in ph and ps, it is not free in (ph \/ ps). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph \/ ps)
Theorem	nf3or 1837	If x is not free in ph, ps, and ch, it is not free in (ph \/ ps \/ ch). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   &   |- F/xps   &   |- F/xch   =>   |- F/x(ph \/ ps \/ ch)
Theorem	equsalhw 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.)
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x(x = y -> ph) <-> ps)
Theorem	equsalhwOLD 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.)
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   =>   |- (A.x(x = y -> ph) <-> ps)
Theorem	19.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.)
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	hbex 1841	If x is not free in ph, it is not free in E.yph. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
Theorem	nfal 1842	If x is not free in ph, it is not free in A.yph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   =>   |- F/xA.yph
Theorem	nfex 1843	If x is not free in ph, it is not free in E.yph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/xph   =>   |- F/xE.yph
Theorem	nfexOLD 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/xph   =>   |- F/xE.yph
Theorem	nfnf 1845	If x is not free in ph, it is not free in F/yph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/xph   =>   |- F/x F/yph
Theorem	nfnfOLD 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/xph   =>   |- F/x F/yph
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 3790. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- (E.xA.yph -> A.yE.xph)
Theorem	19.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.)
|- (E.xA.yph -> A.yE.xph)
Theorem	dvelimhw 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.)
|- (ph -> A.xph)   &   |- (ps -> A.zps)   &   |- (z = y -> (ph <-> ps))   &   |- (-. A.x x = y -> (y = z -> A.x y = z))   =>   |- (-. A.x x = y -> (ps -> A.xps))
Theorem	cbv3hv 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.)
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- (A.xph -> A.yps)
Theorem	cbv3hvOLD 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.)
|- (ph -> A.yph)   &   |- (ps -> A.xps)   &   |- (x = y -> (ph -> ps))   =>   |- (A.xph -> A.yps)
Theorem	nfald 1852	If x is not free in ph, it is not free in A.yph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/xA.yps)
Theorem	nfaldOLD 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/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/xA.yps)
Theorem	nfexd 1854	If x is not free in ph, it is not free in E.yph. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/xE.yps)
Theorem	nfa2 1855	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xA.yA.xph
Theorem	nfia1 1856	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/x(A.xph -> A.xps)
Theorem	19.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/xph -> (E.xph <-> ph))
Theorem	excomimOLD 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.)
|- (E.xE.yph -> E.yE.xph)
Theorem	excomOLD 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.)
|- (E.xE.yph <-> E.yE.xph)
Theorem	19.16 1860	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 1861	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.19 1862	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.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/xph -> (A.x(ph -> ps) <-> (ph -> A.xps)))
Theorem	19.21-2 1864	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
|- F/xph   &   |- F/yph   =>   |- (A.xA.y(ph -> ps) <-> (ph -> A.xA.yps))
Theorem	19.21bbi 1865	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	nf2 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/xph <-> (E.xph -> A.xph))
Theorem	nf3 1867	An alternative definition of df-nf 1545. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/xph <-> A.x(E.xph -> ph))
Theorem	nf4 1868	Variable x is effectively not free in ph iff ph is always true or always false. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/xph <-> (A.xph \/ A.x -. ph))
Theorem	19.27 1869	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28 1870	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.36 1871	Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36i 1872	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   &   |- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.37 1873	Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.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.)
|- ((E.xph -> A.xps) -> A.x(ph -> ps))
Theorem	19.32 1875	Theorem 19.32 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/xph   =>   |- (A.x(ph \/ ps) <-> (ph \/ A.xps))
Theorem	19.31 1876	Theorem 19.31 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (A.x(ph \/ ps) <-> (A.xph \/ ps))
Theorem	19.44 1877	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (E.x(ph \/ ps) <-> (E.xph \/ ps))
Theorem	19.45 1878	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (E.x(ph \/ ps) <-> (ph \/ E.xps))
Theorem	19.41 1879	Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- F/xps   =>   |- (E.x(ph /\ ps) <-> (E.xph /\ ps))
Theorem	19.42 1880	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- F/xph   =>   |- (E.x(ph /\ ps) <-> (ph /\ E.xps))
Theorem	nfan1 1881	A closed form of nfan 1824. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/xph   &   |- (ph -> F/xps)   =>   |- F/x(ph /\ ps)
Theorem	exan 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.)
|- (E.xph /\ ps)   =>   |- E.x(ph /\ ps)
Theorem	hbnd 1883	Deduction form of bound-variable hypothesis builder hbn 1776. (Contributed by NM, 3-Jan-2002.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> (-. ps -> A.x -. ps))
Theorem	aaan 1884	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- F/yph   &   |- F/xps   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	eeor 1885	Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
|- F/yph   &   |- F/xps   =>   |- (E.xE.y(ph \/ ps) <-> (E.xph \/ E.yps))
Theorem	qexmid 1886	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic. (Contributed by NM, 10-Dec-2000.)
|- E.x(ph -> A.xph)
Theorem	equs5a 1887	A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
|- (E.x(x = y /\ A.yph) -> A.x(x = y -> ph))
Theorem	equs5e 1888	A property related to substitution that unlike equs5 1996 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
|- (E.x(x = y /\ ph) -> A.x(x = y -> E.yph))
Theorem	exlimdd 1889	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- F/xph   &   |- F/xch   &   |- (ph -> E.xps)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> ch)
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 F/xph 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.)
|- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.23v 1891*	Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
|- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23vv 1892*	Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
|- (A.xA.y(ph -> ps) <-> (E.xE.yph -> ps))
Theorem	pm11.53 1893*	Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- (A.xA.y(ph -> ps) <-> (E.xph -> A.yps))
Theorem	19.27v 1894*	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
|- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28v 1895*	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
|- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.36v 1896*	Special case of Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36aiv 1897*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.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.)
|- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	19.37v 1899*	Special case of Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.37aiv 1900*	Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- E.x(ph -> ps)   =>   |- (ph -> E.xps)