P. 19 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hbsb3 1801	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1 1802	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sbcof2 1803	Version of sbco 1961 where 𝑥 is not free in 𝜑. (Contributed by Jim Kingdon, 28-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
1.4  Predicate calculus with distinct variables
1.4.1  Derive the axiom of distinct variables ax-16
Theorem	spimv 1804*	A version of spim 1731 with a distinct variable requirement instead of a bound-variable hypothesis. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	aev 1805*	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1807. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	ax16 1806*	Theorem showing that ax-16 1807 is redundant if ax-17 1519 is included in the axiom system. The important part of the proof is provided by aev 1805. See ax16ALT 1852 for an alternate proof that does not require ax-10 1498 or ax12 1505. This theorem should not be referenced in any proof. Instead, use ax-16 1807 below so that theorems needing ax-16 1807 can be more easily identified. (Contributed by NM, 8-Nov-2006.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Axiom	ax-16 1807*	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 1519 to be a metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. It is a somewhat bizarre axiom since the antecedent is always false in set theory, but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-17 1519; see Theorem ax16 1806. This axiom is obsolete and should no longer be used. It is proved above as Theorem ax16 1806. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	dveeq2 1808*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	dveeq2or 1809*	Quantifier introduction when one pair of variables is distinct. Like dveeq2 1808 but connecting ∀𝑥𝑥 = 𝑦 by a disjunction rather than negation and implication makes the theorem stronger in intuitionistic logic. (Contributed by Jim Kingdon, 1-Feb-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥 𝑧 = 𝑦)
Theorem	dvelimfALT2 1810*	Proof of dvelimf 2008 using dveeq2 1808 (shown as the last hypothesis) instead of ax12 1505. This shows that ax12 1505 could be replaced by dveeq2 1808 (the last hypothesis). (Contributed by Andrew Salmon, 21-Jul-2011.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	nd5 1811*	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 8-Jan-2002.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	exlimdv 1812*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	ax11v2 1813*	Recovery of ax11o 1815 from ax11v 1820 without using ax-11 1499. The hypothesis is even weaker than ax11v 1820, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1815. (Contributed by NM, 2-Feb-2007.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax11a2 1814*	Derive ax-11o 1816 from a hypothesis in the form of ax-11 1499. The hypothesis is even weaker than ax-11 1499, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1815. (Contributed by NM, 2-Feb-2007.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
1.4.2  Derive the obsolete axiom of variable substitution ax-11o
Theorem	ax11o 1815	Derivation of set.mm's original ax-11o 1816 from the shorter ax-11 1499 that has replaced it. An open problem is whether this theorem can be proved without relying on ax-16 1807 or ax-17 1519. Normally, ax11o 1815 should be used rather than ax-11o 1816, except by theorems specifically studying the latter's properties. (Contributed by NM, 3-Feb-2007.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Axiom	ax-11o 1816	Axiom ax-11o 1816 ("o" for "old") was the original version of ax-11 1499, before it was discovered (in Jan. 2007) that the shorter ax-11 1499 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. To understand this theorem more easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally meaning "if 𝑥 and 𝑦 are distinct variables, then..." The antecedent becomes false if the same variable is substituted for 𝑥 and 𝑦, ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form ¬ ∀𝑥𝑥 = 𝑦 a "distinctor." This axiom is redundant, as shown by Theorem ax11o 1815. This axiom is obsolete and should no longer be used. It is proved above as Theorem ax11o 1815. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
1.4.3  More theorems related to ax-11 and substitution
Theorem	albidv 1817*	Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbidv 1818*	Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	ax11b 1819	A bidirectional version of ax-11o 1816. (Contributed by NM, 30-Jun-2006.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax11v 1820*	This is a version of ax-11o 1816 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. (Contributed by NM, 5-Aug-1993.) (Revised by Jim Kingdon, 15-Dec-2017.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax11ev 1821*	Analogue to ax11v 1820 for existential quantification. (Contributed by Jim Kingdon, 9-Jan-2018.)
⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑))
Theorem	equs5 1822	Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	equs5or 1823	Lemma used in proofs of substitution properties. Like equs5 1822 but, in intuitionistic logic, replacing negation and implication with disjunction makes this a stronger result. (Contributed by Jim Kingdon, 2-Feb-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ∨ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb3 1824	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
Theorem	sb4 1825	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb4or 1826	One direction of a simplified definition of substitution when variables are distinct. Similar to sb4 1825 but stronger in intuitionistic logic. (Contributed by Jim Kingdon, 2-Feb-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb4b 1827	Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb4bor 1828	Simplified definition of substitution when variables are distinct, expressed via disjunction. (Contributed by Jim Kingdon, 18-Mar-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	hbsb2 1829	Bound-variable hypothesis builder for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	nfsb2or 1830	Bound-variable hypothesis builder for substitution. Similar to hbsb2 1829 but in intuitionistic logic a disjunction is stronger than an implication. (Contributed by Jim Kingdon, 2-Feb-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	sbequilem 1831	Propositional logic lemma used in the sbequi 1832 proof. (Contributed by Jim Kingdon, 1-Feb-2018.)
⊢ (𝜑 ∨ (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜏 ∨ (𝜓 → (𝜃 → 𝜂)))    ⇒   ⊢ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒 → 𝜂))))
Theorem	sbequi 1832	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof modified by Jim Kingdon, 1-Feb-2018.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
Theorem	sbequ 1833	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	drsb2 1834	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	spsbe 1835	A specialization theorem, mostly the same as Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 29-Dec-2017.)
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	spsbim 1836	Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	spsbbi 1837	Specialization of biconditional. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbbidh 1838	Deduction substituting both sides of a biconditional. New proofs should use sbbid 1839 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbbid 1839	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbequ8 1840	Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) (Proof revised by Jim Kingdon, 20-Jan-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbft 1841	Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbid2h 1842	An identity law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbid2 1843	An identity law for substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbidm 1844	An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sb5rf 1845	Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑))
Theorem	sb6rf 1846	Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))
Theorem	sb8h 1847	Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8eh 1848	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 15-Jan-2018.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8 1849	Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8e 1850	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
1.4.4  Predicate calculus with distinct variables (cont.)
Theorem	ax16i 1851*	Inference with ax-16 1807 as its conclusion, that does not require ax-10 1498, ax-11 1499, or ax12 1505 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. (Contributed by NM, 20-May-2008.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	ax16ALT 1852*	Version of ax16 1806 that does not require ax-10 1498 or ax12 1505 for its proof. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	spv 1853*	Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimev 1854*	Distinct-variable version of spime 1734. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	speiv 1855*	Inference from existential specialization, using implicit substitition. (Contributed by NM, 19-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	equvin 1856*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦))
Theorem	a16g 1857*	A generalization of Axiom ax-16 1807. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	a16gb 1858*	A generalization of Axiom ax-16 1807. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑))
Theorem	a16nf 1859*	If there is only one element in the universe, then everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	2albidv 1860*	Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒))
Theorem	2exbidv 1861*	Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))
Theorem	3exbidv 1862*	Formula-building rule for 3 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧𝜓 ↔ ∃𝑥∃𝑦∃𝑧𝜒))
Theorem	4exbidv 1863*	Formula-building rule for 4 existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒))
Theorem	19.9v 1864*	Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 21-May-2007.)
⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	exlimdd 1865	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	19.21v 1866*	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 (𝜑 → ∀𝑥𝜑) in 19.21 1576 via the use of distinct variable conditions combined with ax-17 1519. 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 2024 derived from df-eu 2022. The "f" stands for "not free in" which is less restrictive than "does not occur in". (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	alrimiv 1867*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	alrimivv 1868*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)
Theorem	alrimdv 1869*	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	nfdv 1870*	Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	2ax17 1871*	Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	alimdv 1872*	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	eximdv 1873*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	2alimdv 1874*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	2eximdv 1875*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))
Theorem	19.23v 1876*	Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	19.23vv 1877*	Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓))
Theorem	sb56 1878*	Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1756. (Contributed by NM, 14-Apr-2008.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb6 1879*	Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5 1880*	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sbnv 1881*	Version of sbn 1945 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Dec-2017.)
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
Theorem	sbanv 1882*	Version of sban 1948 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 24-Dec-2017.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	sborv 1883*	Version of sbor 1947 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sbi1v 1884*	Forward direction of sbimv 1886. (Contributed by Jim Kingdon, 25-Dec-2017.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbi2v 1885*	Reverse direction of sbimv 1886. (Contributed by Jim Kingdon, 18-Jan-2018.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	sbimv 1886*	Intuitionistic proof of sbim 1946 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Jan-2018.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblimv 1887*	Version of sblim 1950 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 19-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	pm11.53 1888*	Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))
Theorem	exlimivv 1889*	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)
Theorem	exlimdvv 1890*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))
Theorem	exlimddv 1891*	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	19.27v 1892*	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 1893*	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.36aiv 1894*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.41v 1895*	Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.41vv 1896*	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
Theorem	19.41vvv 1897*	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.41vvvv 1898*	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.42v 1899*	Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	spvv 1900*	Version of spv 1853 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)