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.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
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.)
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
Theorem	exlimi 1803	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxψ    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
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.)
⊢ (ψ → ∀xψ)    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
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.)
⊢ (ψ → ∀xψ)    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	exlimd 1806	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxχ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	exlimdh 1807	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
⊢ (φ → ∀xφ)    &   ⊢ (χ → ∀xχ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	nfimd 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(ψ → χ))
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.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ → χ))
Theorem	hbim1 1810	A closed form of hbim 1817. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
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.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ Ⅎx(φ → ψ)
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.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ Ⅎx(φ → ψ)
Theorem	nfim 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(φ → ψ)
Theorem	nfimOLD 1814	If x 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.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ → ψ)
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.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))
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.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))
Theorem	hbim 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(φ → ψ))
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.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
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.)
⊢ (Ⅎxψ → (∀x(φ → ψ) ↔ (∃xφ → ψ)))
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.)
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
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.)
⊢ (φ → ∀xφ)    &   ⊢ (x = z → (φ → ψ))    ⇒   ⊢ (φ → ∃xψ)
Theorem	nfand 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(ψ ∧ χ))
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.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → Ⅎxθ)    ⇒   ⊢ (φ → Ⅎx(ψ ∧ χ ∧ θ))
Theorem	nfan 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(φ ∧ ψ)
Theorem	nfnan 1825	If x is not free in φ and ψ, then it is not free in (φ ⊼ ψ). (Contributed by Scott Fenton, 2-Jan-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ⊼ ψ)
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.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ∧ ψ)
Theorem	nf3an 1827	If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ). (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎxχ    ⇒   ⊢ Ⅎx(φ ∧ ψ ∧ χ)
Theorem	hban 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(φ ∧ ψ))
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.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ))
Theorem	hb3an 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(φ ∧ ψ ∧ χ))
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.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → ∀x(φ ∧ ψ ∧ χ))
Theorem	nfbid 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(ψ ↔ χ))
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.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ ↔ χ))
Theorem	nfbi 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(φ ↔ ψ)
Theorem	nfbiOLD 1835	If x 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.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ↔ ψ)
Theorem	nfor 1836	If x is not free in φ and ψ, it is not free in (φ ∨ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ∨ ψ)
Theorem	nf3or 1837	If x is not free in φ, ψ, and χ, it is not free in (φ ∨ ψ ∨ χ). (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎxχ    ⇒   ⊢ Ⅎx(φ ∨ ψ ∨ χ)
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.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x(x = y → φ) ↔ ψ)
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.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x(x = y → φ) ↔ ψ)
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.)
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
Theorem	hbex 1841	If x is not free in φ, it is not free in ∃yφ. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    ⇒   ⊢ (∃yφ → ∀x∃yφ)
Theorem	nfal 1842	If x is not free in φ, it is not free in ∀yφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∀yφ
Theorem	nfex 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φ    ⇒   ⊢ Ⅎx∃yφ
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.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃yφ
Theorem	nfnf 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φ    ⇒   ⊢ ℲxℲyφ
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.)
⊢ Ⅎxφ    ⇒   ⊢ ℲxℲyφ
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.)
⊢ (∃x∀yφ → ∀y∃xφ)
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.)
⊢ (∃x∀yφ → ∀y∃xφ)
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.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀zψ)    &   ⊢ (z = y → (φ ↔ ψ))    &   ⊢ (¬ ∀x x = y → (y = z → ∀x y = z))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
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.)
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ∀yψ)
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.)
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ∀yψ)
Theorem	nfald 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ψ)    ⇒   ⊢ (φ → Ⅎx∀yψ)
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.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∀yψ)
Theorem	nfexd 1854	If x is not free in φ, it is not free in ∃yφ. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃yψ)
Theorem	nfa2 1855	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎx∀y∀xφ
Theorem	nfia1 1856	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎx(∀xφ → ∀xψ)
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.)
⊢ (Ⅎxφ → (∃xφ ↔ φ))
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.)
⊢ (∃x∃yφ → ∃y∃xφ)
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.)
⊢ (∃x∃yφ ↔ ∃y∃xφ)
Theorem	19.16 1860	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∀xψ))
Theorem	19.17 1861	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ψ))
Theorem	19.19 1862	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∃xψ))
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.)
⊢ (Ⅎxφ → (∀x(φ → ψ) ↔ (φ → ∀xψ)))
Theorem	19.21-2 1864	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎxφ    &   ⊢ Ⅎyφ    ⇒   ⊢ (∀x∀y(φ → ψ) ↔ (φ → ∀x∀yψ))
Theorem	19.21bbi 1865	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
⊢ (φ → ∀x∀yψ)    ⇒   ⊢ (φ → ψ)
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.)
⊢ (Ⅎxφ ↔ (∃xφ → ∀xφ))
Theorem	nf3 1867	An alternative definition of df-nf 1545. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎxφ ↔ ∀x(∃xφ → φ))
Theorem	nf4 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 ¬ φ))
Theorem	19.27 1869	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ))
Theorem	19.28 1870	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ))
Theorem	19.36 1871	Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∃x(φ → ψ) ↔ (∀xφ → ψ))
Theorem	19.36i 1872	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    &   ⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
Theorem	19.37 1873	Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∃x(φ → ψ) ↔ (φ → ∃xψ))
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.)
⊢ ((∃xφ → ∀xψ) → ∀x(φ → ψ))
Theorem	19.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ψ))
Theorem	19.31 1876	Theorem 19.31 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ ∨ ψ) ↔ (∀xφ ∨ ψ))
Theorem	19.44 1877	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ψ))
Theorem	19.45 1878	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∃x(φ ∨ ψ) ↔ (φ ∨ ∃xψ))
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.)
⊢ Ⅎxψ    ⇒   ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))
Theorem	19.42 1880	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∃x(φ ∧ ψ) ↔ (φ ∧ ∃xψ))
Theorem	nfan1 1881	A closed form of nfan 1824. (Contributed by Mario Carneiro, 3-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ Ⅎx(φ ∧ ψ)
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.)
⊢ (∃xφ ∧ ψ)    ⇒   ⊢ ∃x(φ ∧ ψ)
Theorem	hbnd 1883	Deduction form of bound-variable hypothesis builder hbn 1776. (Contributed by NM, 3-Jan-2002.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ (φ → (¬ ψ → ∀x ¬ ψ))
Theorem	aaan 1884	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ))
Theorem	eeor 1885	Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (∃x∃y(φ ∨ ψ) ↔ (∃xφ ∨ ∃yψ))
Theorem	qexmid 1886	Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic. (Contributed by NM, 10-Dec-2000.)
⊢ ∃x(φ → ∀xφ)
Theorem	equs5a 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 → φ))
Theorem	equs5e 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 = y → ∃yφ))
Theorem	exlimdd 1889	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ Ⅎxφ    &   ⊢ Ⅎxχ    &   ⊢ (φ → ∃xψ)    &   ⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (φ → χ)
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 Ⅎ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ψ))
Theorem	19.23v 1891*	Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
Theorem	19.23vv 1892*	Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
⊢ (∀x∀y(φ → ψ) ↔ (∃x∃yφ → ψ))
Theorem	pm11.53 1893*	Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀x∀y(φ → ψ) ↔ (∃xφ → ∀yψ))
Theorem	19.27v 1894*	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ))
Theorem	19.28v 1895*	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ))
Theorem	19.36v 1896*	Special case of Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ (∃x(φ → ψ) ↔ (∀xφ → ψ))
Theorem	19.36aiv 1897*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
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.)
⊢ (∃x∀y(φ → ψ) ↔ ∀y∃x(φ → ψ))
Theorem	19.37v 1899*	Special case of Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃x(φ → ψ) ↔ (φ → ∃xψ))
Theorem	19.37aiv 1900*	Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃x(φ → ψ)    ⇒   ⊢ (φ → ∃xψ)