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
1.4.2  Rule scheme ax-gen (Generalization)
Axiom	ax-gen 1801	Rule of (universal) generalization. In our axiomatization, this is the only postulated (that is, axiomatic) rule of inference of predicate calculus (together with the rule of modus ponens ax-mp 5 of propositional calculus). See, e.g., Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved 𝑥 = 𝑥, then we can conclude ∀𝑥𝑥 = 𝑥 or even ∀𝑦𝑥 = 𝑥. Theorem altru 1813 shows the special case ∀𝑥⊤. The converse rule of inference spi 2180 (universal instantiation, or universal specialization) shows that we can also go the other way: in other words, we can add or remove universal quantifiers from the beginning of any theorem as required. Note that the closed form (𝜑 → ∀𝑥𝜑) need not hold (but may hold in special cases, see ax-5 1916). (Contributed by NM, 3-Jan-1993.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	gen2 1802	Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
⊢ 𝜑    ⇒   ⊢ ∀𝑥∀𝑦𝜑
Theorem	mpg 1803	Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)
⊢ (∀𝑥𝜑 → 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	mpgbi 1804	Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
⊢ (∀𝑥𝜑 ↔ 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	mpgbir 1805	Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
⊢ (𝜑 ↔ ∀𝑥𝜓)    &   ⊢ 𝜓    ⇒   ⊢ 𝜑
Theorem	nex 1806	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ ∃𝑥𝜑
Theorem	nfth 1807	No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1790 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfnth 1808	No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.) df-nf 1790 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ ¬ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	hbth 1809	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 1807), but keeps its interest in some cases. (Revised by BJ, 23-Sep-2022.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nftru 1810	The true constant has no free variables. (This can also be proven in one step with nfv 1920, but this proof does not use ax-5 1916.) (Contributed by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥⊤
Theorem	nffal 1811	The false constant has no free variables (see nftru 1810). (Contributed by BJ, 6-May-2019.)
⊢ Ⅎ𝑥⊥
Theorem	sptruw 1812	Version of sp 2179 when 𝜑 is true. Instance of a1i 11. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.)
⊢ 𝜑    ⇒   ⊢ (∀𝑥𝜑 → 𝜑)
Theorem	altru 1813	For all sets, ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∀𝑥⊤
Theorem	alfal 1814	For all sets, ¬ ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∀𝑥 ¬ ⊥
1.4.3  Axiom scheme ax-4 (Quantified Implication)
Axiom	ax-4 1815	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1816 for labeling consistency. It should be used only by alim 1816. (Contributed by NM, 21-May-2008.) Use alim 1816 instead. (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alim 1816	Restatement of Axiom ax-4 1815, for labeling consistency. It should be the only theorem using ax-4 1815. (Contributed by NM, 10-Jan-1993.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alimi 1817	Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	2alimi 1818	Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)
Theorem	ala1 1819	Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜑))
Theorem	al2im 1820	Closed form of al2imi 1821. Version of alim 1816 for a nested implication. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	al2imi 1821	Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alanimi 1822	Variant of al2imi 1821 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒)
Theorem	alimdh 1823	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1816. (Contributed by NM, 4-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	albi 1824	Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	albii 1825	Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Theorem	2albii 1826	Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)
Theorem	sylgt 1827	Closed form of sylg 1828. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜓 → 𝜒) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒)))
Theorem	sylg 1828	A syllogism combined with generalization. Inference associated with sylgt 1827. General form of alrimih 1829. (Contributed by BJ, 4-Oct-2019.)
⊢ (𝜑 → ∀𝑥𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	alrimih 1829	Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2203 and 19.21h 2287. Instance of sylg 1828. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	hbxfrbi 1830	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2870 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	alex 1831	Universal quantifier in terms of existential quantifier and negation. Dual of df-ex 1786. See also the dual pair alnex 1787 / exnal 1832. Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
Theorem	exnal 1832	Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1787. See also the dual pair df-ex 1786 / alex 1831. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Theorem	2nalexn 1833	Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∀𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦 ¬ 𝜑)
Theorem	2exnaln 1834	Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	2nexaln 1835	Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
Theorem	alimex 1836	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 nonfreeness. See also eximal 1788. (Contributed by BJ, 12-May-2019.)
⊢ ((𝜑 → ∀𝑥𝜓) ↔ (∃𝑥 ¬ 𝜓 → ¬ 𝜑))
Theorem	aleximi 1837	A variant of al2imi 1821: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2151, sps 2181 and eximd 2212, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	alexbii 1838	Biconditional form of aleximi 1837. (Contributed by BJ, 16-Nov-2020.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exim 1839	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	eximi 1840	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	2eximi 1841	Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)
Theorem	eximii 1842	Inference associated with eximi 1840. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	exa1 1843	Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.)
⊢ (∃𝑥𝜑 → ∃𝑥(𝜓 → 𝜑))
Theorem	19.38 1844	Theorem 19.38 of [Margaris] p. 90. The converse holds under nonfreeness conditions, see 19.38a 1845 and 19.38b 1846. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 2202. (Revised by Wolf Lammen, 2-Jan-2018.)
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	19.38a 1845	Under a nonfreeness hypothesis, the implication 19.38 1844 can be strengthened to an equivalence. See also 19.38b 1846. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
⊢ (Ⅎ𝑥𝜑 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	19.38b 1846	Under a nonfreeness hypothesis, the implication 19.38 1844 can be strengthened to an equivalence. See also 19.38a 1845. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.)
⊢ (Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓)))
Theorem	imnang 1847	Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥 ¬ (𝜑 ∧ 𝜓))
Theorem	alinexa 1848	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	exnalimn 1849	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 1850	A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.)
⊢ (∀𝑥∃𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∀𝑦𝜑)
Theorem	2exnexn 1851	Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.)
⊢ (∃𝑥∀𝑦𝜑 ↔ ¬ ∀𝑥∃𝑦 ¬ 𝜑)
Theorem	exbi 1852	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	exbii 1853	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Theorem	2exbii 1854	Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)
Theorem	3exbii 1855	Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)
Theorem	nfbiit 1856	Equivalence theorem for the nonfreeness predicate. Closed form of nfbii 1857. (Contributed by Giovanni Mascellani, 10-Apr-2018.) Reduce axiom usage. (Revised by BJ, 6-May-2019.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	nfbii 1857	Equality theorem for the nonfreeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1790 changed. (Revised by Wolf Lammen, 12-Sep-2021.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
Theorem	nfxfr 1858	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	nfxfrd 1859	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜒 → Ⅎ𝑥𝜑)
Theorem	nfnbi 1860	A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 6-Oct-2024.)
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑)
Theorem	nfnbiOLD 1861	Obsolete version of nfnbi 1860 as of 6-Oct-2024. (Contributed by BJ, 6-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑)
Theorem	nfnt 1862	If a variable is nonfree in a proposition, then it is nonfree 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 1790 changed. (Revised by Wolf Lammen, 4-Oct-2021.)
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
Theorem	nfn 1863	Inference associated with nfnt 1862. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1790 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 ¬ 𝜑
Theorem	nfnd 1864	Deduction associated with nfnt 1862. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Theorem	exanali 1865	A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓))
Theorem	2exanali 1866	Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (¬ ∃𝑥∃𝑦(𝜑 ∧ ¬ 𝜓) ↔ ∀𝑥∀𝑦(𝜑 → 𝜓))
Theorem	exancom 1867	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
Theorem	exan 1868	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	alrimdh 1869	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2203 and 19.21h 2287. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximdh 1870	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	nexdh 1871	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	albidh 1872	Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbidh 1873	Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exsimpl 1874	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
Theorem	exsimpr 1875	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓)
Theorem	19.26 1876	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 1877	Theorem 19.26 1876 with two quantifiers. (Contributed by NM, 3-Feb-2005.)
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓))
Theorem	19.26-3an 1878	Theorem 19.26 1876 with triple conjunction. (Contributed by NM, 13-Sep-2011.)
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	19.29 1879	Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1880. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r 1880	Variation of 19.29 1879. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r2 1881	Variation of 19.29r 1880 with double quantification. (Contributed by NM, 3-Feb-2005.)
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.29x 1882	Variation of 19.29 1879 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.35 1883	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 1884	Inference associated with 19.35 1883. (Contributed by NM, 21-Jun-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∃𝑥𝜓)
Theorem	19.35ri 1885	Inference associated with 19.35 1883. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑥𝜑 → ∃𝑥𝜓)    ⇒   ⊢ ∃𝑥(𝜑 → 𝜓)
Theorem	19.25 1886	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓))
Theorem	19.30 1887	Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.43 1888	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.43OLD 1889	Obsolete proof of 19.43 1888. Do not delete as it is referenced on the mmrecent.html 1888 page and in conventions-labels 28744. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.33 1890	Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓))
Theorem	19.33b 1891	The antecedent provides a condition implying the converse of 19.33 1890. (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 1892	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
Theorem	19.40-2 1893	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 1894	The antecedent provides a condition implying the converse of 19.40 1892. This is to 19.40 1892 what 19.33b 1891 is to 19.33 1890. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.)
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	albiim 1895	Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜑)))
Theorem	2albiim 1896	Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005.)
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) ↔ (∀𝑥∀𝑦(𝜑 → 𝜓) ∧ ∀𝑥∀𝑦(𝜓 → 𝜑)))
Theorem	exintrbi 1897	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	exintr 1898	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 1899	Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒))
Theorem	nfimd 1900	If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1902. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1790 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1901. (Revised by Wolf Lammen, 10-Jul-2022.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))