P. 19 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hba1OLD 1801	Obsolete proof of hba1 1800 as of 15-Dec-2017 (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x ph -> A. x A. x ph )
Theorem	nfa1 1802	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x A. x ph
Theorem	a5i 1803	Inference version of ax5o 1761. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	nfnf1 1804	x is not free in F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/ x ph
Theorem	nfnd 1805	If in a context x is not free in ps, it is not free in -. ps. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfndOLD 1806	Obsolete proof of nfnd 1805 as of 28-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfn 1807	If x is not free in ph, it is not free in -. ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	19.38 1808	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 2-Jan-2018.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
Theorem	19.21t 1809	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21 1810	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	19.21h 1811	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph." (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	stdpc5 1812	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis F/ x ph can be thought of as emulating " x is not free in ph." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by nfequid 1686. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	stdpc5OLD 1813	Obsolete proof of stdpc5 1812 as of 1-Jan-2018. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	19.23t 1814	Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- ( F/ x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23 1815	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.23h 1816	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. x ps )   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	exlimi 1817	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimih 1818	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. x ps )   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimihOLD 1819	Obsolete proof of exlimih 1818 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimd 1820	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdOLD 1821	Obsolete proof of exlimd 1820 as of 12-Jan-2018. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdh 1822	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.)
|- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	nfimd 1823	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/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps -> ch ) )
Theorem	nfimdOLD 1824	Obsolete proof of nfimd 1823 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps -> ch ) )
Theorem	hbim1 1825	A closed form of hbim 1832. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1826	A closed form of nfim 1828. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfim1OLD 1827	A closed form of nfim 1828. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfim 1828	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/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	nfimOLD 1829	If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	hbimd 1830	Deduction form of bound-variable hypothesis builder hbim 1832. (Contributed by NM, 1-Jan-2002.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	hbimdOLD 1831	Obsolete proof of hbimd 1830 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	hbim 1832	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. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	hbimOLD 1833	Obsolete proof of hbim 1832 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	19.23tOLD 1834	Obsolete proof of 19.23t 1814 as of 1-Jan-2018. (Contributed by NM, 7-Nov-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23hOLD 1835	Obsolete proof of 19.23h 1816 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	spimehOLD 1836*	Obsolete proof of spimeh 1675 as of 10-Dec-2017. (Contributed by NM, 7-Aug-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( x = z -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	19.27 1837	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28 1838	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	nfand 1839	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/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps /\ ch ) )
Theorem	nf3and 1840	Deduction form of bound-variable hypothesis builder nf3an 1845. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/ x th )   =>    |- ( ph -> F/ x ( ps /\ ch /\ th ) )
Theorem	nfan1 1841	A closed form of nfan 1842. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1842	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, 13-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nfnan 1843	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/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -/\ ps )
Theorem	nfanOLD 1844	Obsolete proof of nfan 1842 as of 2-Jan-2018. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nf3an 1845	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/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph /\ ps /\ ch )
Theorem	hban 1846	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. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hbanOLD 1847	Obsolete proof of hban 1846 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hb3an 1848	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. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	hb3anOLD 1849	Obsolete proof of hb3an 1848 as of 2-Jan-2018. (Contributed by NM, 14-Sep-2003.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	nfbid 1850	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/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps <-> ch ) )
Theorem	nfbidOLD 1851	Obsolete proof of nfbid 1850 as of 29-Dec-2017. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps <-> ch ) )
Theorem	nfbi 1852	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/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph <-> ps )
Theorem	nfbiOLD 1853	If x is not free in ph and ps, it is not free in ( ph <-> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph <-> ps )
Theorem	nfor 1854	If x is not free in ph and ps, it is not free in ( ph \/ ps ). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph \/ ps )
Theorem	nf3or 1855	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/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph \/ ps \/ ch )
Theorem	equsalhw 1856*	Weaker version of equsalh 1968 (requiring distinct variables) without using ax-12 1946. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 28-Dec-2017.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsalhwOLD 1857*	Obsolete proof of equsalhw 1856 as of 28-Dec-2017. (Contributed by NM, 29-Nov-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ps -> A. x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	19.21hOLD 1858	Obsolete proof of 19.21h 1811 as of 1-Jan-2018. (Contributed by NM, 1-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	hbex 1859	If x is not free in ph, it is not free in E. y ph. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfal 1860	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x A. y ph
Theorem	nfex 1861	If x is not free in ph, it is not free in E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	nfexOLD 1862	Obsolete proof of nfex 1861 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	nfnf 1863	If x is not free in ph, it is not free in F/ y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x F/ y ph
Theorem	nfnfOLD 1864	Obsolete proof of nfnf 1863 as of 30-Dec-2017. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- F/ x F/ y ph
Theorem	19.12 1865	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 1917 and r19.12sn 3832. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
|- ( E. x A. y ph -> A. y E. x ph )
Theorem	19.12OLD 1866	Obsolete proof of 19.12 1865 as of 3-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E. x A. y ph -> A. y E. x ph )
Theorem	nfald 1867	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 6-Jan-2018.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfaldOLD 1868	Obsolete proof of nfald 1867 as of 6-Jan-2018. (Contributed by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfexd 1869	If x is not free in ph, it is not free in E. y ph. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y ps )
Theorem	nfa2 1870	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x A. y A. x ph
Theorem	nfia1 1871	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ( A. x ph -> A. x ps )
Theorem	dvelimhw 1872*	Proof of dvelimh 2015 without using ax-12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   &    |- ( -. A. x x = y -> ( y = z -> A. x y = z ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimhwOLD 1873*	Proof of dvelimh 2015 without using ax-12 1946 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   &    |- ( -. A. x x = y -> ( y = z -> A. x y = z ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	cbv3hv 1874*	Lemma for ax10 1991. Similar to cbv3h 2036. Requires distinct variables but avoids ax-12 1946. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	cbv3hvOLD 1875*	Obsolete proof of cbv3hv 1874 as of 29-Dec-2017. (Contributed by NM, 25-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	19.9tOLD 1876	Obsolete proof of 19.9t 1789 as of 30-Dec-2017. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( E. x ph <-> ph ) )
Theorem	excomimOLD 1877	Obsolete proof of excomim 1753 as of 8-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E. x E. y ph -> E. y E. x ph )
Theorem	excomOLD 1878	Obsolete proof of excom 1752 as of 8-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E. x E. y ph <-> E. y E. x ph )
Theorem	19.16 1879	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) )
Theorem	19.17 1880	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) )
Theorem	19.19 1881	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) )
Theorem	19.21tOLD 1882	Obsolete proof of 19.21t 1809 as of 30-Dec-2017. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21-2 1883	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
|- F/ x ph   &    |- F/ y ph   =>    |- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )
Theorem	19.21bbi 1884	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> A. x A. y ps )   =>    |- ( ph -> ps )
Theorem	nf2 1885	An alternative definition of df-nf 1551, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
Theorem	nf3 1886	An alternative definition of df-nf 1551. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> A. x ( E. x ph -> ph ) )
Theorem	nf4 1887	Variable x is effectively not free in ph iff ph is always true or always false. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
Theorem	19.36 1888	Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
Theorem	19.36i 1889	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   &    |- E. x ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	19.37 1890	Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) )
Theorem	19.38OLD 1891	Obsolete proof of 19.38 1808 as of 2-Jan-2018. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
Theorem	19.32 1892	Theorem 19.32 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) )
Theorem	19.31 1893	Theorem 19.31 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( A. x ( ph \/ ps ) <-> ( A. x ph \/ ps ) )
Theorem	19.44 1894	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45 1895	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	19.41 1896	Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
|- F/ x ps   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.41OLD 1897	Obsolete proof of 19.41 1896 as of 12-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ps   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.42 1898	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	exan 1899	Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
|- ( E. x ph /\ ps )   =>    |- E. x ( ph /\ ps )
Theorem	exanOLD 1900	Obsolete proof of exan 1899 as of 13-Jan-2018. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E. x ph /\ ps )   =>    |- E. x ( ph /\ ps )