P. 19 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	nex 1801	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ ∃𝑥𝜑
Theorem	nfth 1802	No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1785 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfnth 1803	No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.) df-nf 1785 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	hbth 1804	No variable is (effectively) free in a theorem. This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form ⊢ (𝜑 → ∀𝑥𝜑) from smaller formulas of this form. These are useful for constructing hypotheses that state "𝑥 is (effectively) not free in 𝜑". (Contributed by NM, 11-May-1993.) This hb* idiom is generally being replaced by the nf* idiom (see nfth 1802), but keeps its interest in some cases. (Revised by BJ, 23-Sep-2022.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nftru 1805	The true constant has no free variables. (This can also be proven in one step with nfv 1915, but this proof does not use ax-5 1911.) (Contributed by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥⊤
Theorem	nffal 1806	The false constant has no free variables (see nftru 1805). (Contributed by BJ, 6-May-2019.)
⊢ Ⅎ𝑥⊥
Theorem	sptruw 1807	Version of sp 2182 when 𝜑 is true. Instance of a1i 11. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.)
⊢ 𝜑    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	altru 1808	For all sets, ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∀𝑥⊤
Theorem	alfal 1809	For all sets, ¬ ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∀𝑥 ¬ ⊥
1.4.3  Axiom scheme ax-4 (Quantified Implication)
Axiom	ax-4 1810	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1811 for labeling consistency. It should be used only by alim 1811. (Contributed by NM, 21-May-2008.) Use alim 1811 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alim 1811	Restatement of Axiom ax-4 1810, for labeling consistency. It should be the only theorem using ax-4 1810. (Contributed by NM, 10-Jan-1993.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alimi 1812	Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	2alimi 1813	Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)
Theorem	ala1 1814	Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜑))
Theorem	al2im 1815	Closed form of al2imi 1816. Version of alim 1811 for a nested implication. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	al2imi 1816	Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alanimi 1817	Variant of al2imi 1816 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)
Theorem	alimdh 1818	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1811. (Contributed by NM, 4-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	albi 1819	Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	albii 1820	Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Theorem	2albii 1821	Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)
Theorem	sylgt 1822	Closed form of sylg 1823. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜓 → 𝜒) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒)))
Theorem	sylg 1823	A syllogism combined with generalization. Inference associated with sylgt 1822. General form of alrimih 1824. (Contributed by BJ, 4-Oct-2019.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	alrimih 1824	Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2207 and 19.21h 2295. Instance of sylg 1823. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	hbxfrbi 1825	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2944 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	alex 1826	Universal quantifier in terms of existential quantifier and negation. Dual of df-ex 1781. See also the dual pair alnex 1782 / exnal 1827. Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
Theorem	exnal 1827	Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1782. See also the dual pair df-ex 1781 / alex 1826. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Theorem	2nalexn 1828	Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∀𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦 ¬ 𝜑)
Theorem	2exnaln 1829	Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	2nexaln 1830	Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	alimex 1831	An equivalence between an implication with a universally quantified consequent and an implication with an existentially quantified antecedent. An interesting case is when the same formula is substituted for both 𝜑 and 𝜓, since then both implications express a type of non-freeness. See also eximal 1783. (Contributed by BJ, 12-May-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) ↔ (∃𝑥 ¬ 𝜓 → ¬ 𝜑))
Theorem	aleximi 1832	A variant of al2imi 1816: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2155, sps 2184 and eximd 2216, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	alexbii 1833	Biconditional form of aleximi 1832. (Contributed by BJ, 16-Nov-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exim 1834	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	eximi 1835	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	2eximi 1836	Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)
Theorem	eximii 1837	Inference associated with eximi 1835. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	exa1 1838	Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.)
⊢ (∃𝑥𝜑 → ∃𝑥(𝜓 → 𝜑))
Theorem	19.38 1839	Theorem 19.38 of [Margaris] p. 90. The converse holds under non-freeness conditions, see 19.38a 1840 and 19.38b 1841. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 2206. (Revised by Wolf Lammen, 2-Jan-2018.)
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	19.38a 1840	Under a non-freeness hypothesis, the implication 19.38 1839 can be strengthened to an equivalence. See also 19.38b 1841. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
⊢ (Ⅎ𝑥𝜑 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	19.38b 1841	Under a non-freeness hypothesis, the implication 19.38 1839 can be strengthened to an equivalence. See also 19.38a 1840. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
⊢ (Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	imnang 1842	Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥 ¬ (𝜑 ∧ 𝜓))
Theorem	alinexa 1843	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	exnalimn 1844	Existential quantification of a conjunction expressed with only primitive symbols (→, ¬, ∀). (Contributed by NM, 10-May-1993.) State the most general instance. (Revised by BJ, 29-Sep-2019.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓))
Theorem	alexn 1845	A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.)
⊢ (∀𝑥∃𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∀𝑦𝜑)
Theorem	2exnexn 1846	Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.)
⊢ (∃𝑥∀𝑦𝜑 ↔ ¬ ∀𝑥∃𝑦 ¬ 𝜑)
Theorem	exbi 1847	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	exbii 1848	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Theorem	2exbii 1849	Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)
Theorem	3exbii 1850	Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)
Theorem	nfbiit 1851	Equivalence theorem for the non-freeness predicate. Closed form of nfbii 1852. (Contributed by Giovanni Mascellani, 10-Apr-2018.) Reduce axiom usage. (Revised by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	nfbii 1852	Equality theorem for the non-freeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1785 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
Theorem	nfxfr 1853	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfxfrd 1854	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜒 → Ⅎ𝑥𝜑)
Theorem	nfnbi 1855	A variable is non-free in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019.)
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑)
Theorem	nfnt 1856	If a variable is non-free in a proposition, then it is non-free in its negation. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) df-nf 1785 changed. (Revised by Wolf Lammen, 4-Oct-2021.)
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
Theorem	nfn 1857	Inference associated with nfnt 1856. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1785 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 ¬ 𝜑
Theorem	nfnd 1858	Deduction associated with nfnt 1856. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Theorem	exanali 1859	A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
Theorem	2exanali 1860	Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦(𝜑 ∧ ¬ 𝜓) ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	exancom 1861	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
Theorem	exan 1862	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.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof shortened by Wolf Lammen, 6-Nov-2022.) Expand hypothesis. (Revised by Steven Nguyen, 19-Jun-2023.)
⊢ ∃𝑥𝜑    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥(𝜑 ∧ 𝜓)
Theorem	exanOLD 1863	Obsolete proof of exan 1862 as of 19-Jun-2023. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof shortened by Wolf Lammen, 6-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥𝜑 ∧ 𝜓)    ⇒   ⊢ ∃𝑥(𝜑 ∧ 𝜓)
Theorem	alrimdh 1864	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2207 and 19.21h 2295. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximdh 1865	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	nexdh 1866	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albidh 1867	Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbidh 1868	Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exsimpl 1869	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
Theorem	exsimpr 1870	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓)
Theorem	19.26 1871	Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Theorem	19.26-2 1872	Theorem 19.26 1871 with two quantifiers. (Contributed by NM, 3-Feb-2005.)
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓))
Theorem	19.26-3an 1873	Theorem 19.26 1871 with triple conjunction. (Contributed by NM, 13-Sep-2011.)
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	19.29 1874	Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1875. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r 1875	Variation of 19.29 1874. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r2 1876	Variation of 19.29r 1875 with double quantification. (Contributed by NM, 3-Feb-2005.)
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.29x 1877	Variation of 19.29 1874 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.35 1878	Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	19.35i 1879	Inference associated with 19.35 1878. (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∃𝑥𝜓)
Theorem	19.35ri 1880	Inference associated with 19.35 1878. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥𝜑 → ∃𝑥𝜓)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜓)
Theorem	19.25 1881	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓))
Theorem	19.30 1882	Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.43 1883	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.43OLD 1884	Obsolete proof of 19.43 1883. Do not delete as it is referenced on the mmrecent.html 1883 page and in conventions-labels 28182. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.33 1885	Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓))
Theorem	19.33b 1886	The antecedent provides a condition implying the converse of 19.33 1885. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.)
⊢ (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Theorem	19.40 1887	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
Theorem	19.40-2 1888	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with two quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	19.40b 1889	The antecedent provides a condition implying the converse of 19.40 1887. This is to 19.40 1887 what 19.33b 1886 is to 19.33 1885. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.)
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	albiim 1890	Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜑)))
Theorem	2albiim 1891	Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) ↔ (∀𝑥∀𝑦(𝜑 → 𝜓) ∧ ∀𝑥∀𝑦(𝜓 → 𝜑)))
Theorem	exintrbi 1892	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	exintr 1893	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) (Proof shortened by BJ, 16-Sep-2022.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	alsyl 1894	Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒))
Theorem	nfimd 1895	If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1897. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1785 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1896. (Revised by Wolf Lammen, 10-Jul-2022.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
Theorem	nfimt 1896	Closed form of nfim 1897 and nfimd 1895. (Contributed by BJ, 20-Oct-2021.) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6-Jul-2022.)
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
Theorem	nfim 1897	If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1896. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1785 changed. (Revised by Wolf Lammen, 17-Sep-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfand 1898	If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))
Theorem	nf3and 1899	Deduction form of bound-variable hypothesis builder nf3an 1902. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝜃)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	nfan 1900	If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)