P. 20 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1901-2000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	alrimivv 1901*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)
Theorem	alrimdv 1902*	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	nfdv 1903*	Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	2ax17 1904*	Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜑)
Theorem	alimdv 1905*	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	eximdv 1906*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	2alimdv 1907*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	2eximdv 1908*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒))
Theorem	19.23v 1909*	Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	19.23vv 1910*	Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓))
Theorem	sbbidv 1911*	Deduction substituting both sides of a biconditional, with 𝜑 and 𝑥 disjoint. See also sbbid 1872. (Contributed by Wolf Lammen, 6-May-2023.) (Proof shortened by Steven Nguyen, 6-Jul-2023.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑡 / 𝑥]𝜓 ↔ [𝑡 / 𝑥]𝜒))
Theorem	sb56 1912*	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 1789. (Contributed by NM, 14-Apr-2008.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb6 1913*	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 1914*	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 1915*	Version of sbn 1983 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Dec-2017.)
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
Theorem	sbanv 1916*	Version of sban 1986 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 24-Dec-2017.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	sborv 1917*	Version of sbor 1985 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sbi1v 1918*	Forward direction of sbimv 1920. (Contributed by Jim Kingdon, 25-Dec-2017.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbi2v 1919*	Reverse direction of sbimv 1920. (Contributed by Jim Kingdon, 18-Jan-2018.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	sbimv 1920*	Intuitionistic proof of sbim 1984 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Jan-2018.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblimv 1921*	Version of sblim 1988 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 19-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	pm11.53 1922*	Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))
Theorem	exlimivv 1923*	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → 𝜓)
Theorem	exlimdvv 1924*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))
Theorem	exlimddv 1925*	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
⊢ (𝜑 → ∃𝑥𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	19.27v 1926*	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28v 1927*	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.36aiv 1928*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.41v 1929*	Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.41vv 1930*	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
Theorem	19.41vvv 1931*	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.41vvvv 1932*	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.42v 1933*	Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	spvv 1934*	Version of spv 1886 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarvv 1935*	Version of chvarv 1968 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	exdistr 1936*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	exdistrv 1937*	Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1929 and 19.42v 1933. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1963. (Contributed by BJ, 30-Sep-2022.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	19.42vv 1938*	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	19.42vvv 1939*	Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	19.42vvvv 1940*	Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑤∃𝑥∃𝑦∃𝑧𝜓))
Theorem	exdistr2 1941*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓))
Theorem	3exdistr 1942*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒)))
Theorem	4exdistr 1943*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃))))
Theorem	cbvalv 1944*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv 1945*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvalvw 1946*	Change bound variable. See cbvalv 1944 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1474. (Revised by GG, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexvw 1947*	Change bound variable. See cbvexv 1945 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1474. (Revised by GG, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbval2 1948*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2 1949*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbval2v 1950*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2v 1951*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvald 1952*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2048. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdh 1953*	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 2048. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvexd 1954*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2048. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldva 1955*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdva 1956*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldvaw 1957*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 1955 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdvaw 1958*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 1956 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2vw 1959*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vw 1960*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) (Revised by GG, 10-Jan-2024.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4v 1961*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	eean 1962	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeanv 1963*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeeanv 1964*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))
Theorem	ee4anv 1965*	Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓))
Theorem	ee8anv 1966*	Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ∧ ∃𝑣∃𝑢∃𝑡∃𝑠𝜓))
Theorem	nexdv 1967*	Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	chvarv 1968*	Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
1.4.5  More substitution theorems
Theorem	hbs1 1969*	𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 5-Aug-1993.) (Proof by Jim Kingdon, 16-Dec-2017.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1v 1970*	𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sbhb 1971*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by NM, 29-May-2009.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))
Theorem	hbsbv 1972*	This is a version of hbsb 1980 with an extra distinct variable constraint, on 𝑧 and 𝑥. (Contributed by Jim Kingdon, 25-Dec-2017.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfsbxy 1973*	Similar to hbsb 1980 but with an extra distinct variable constraint, on 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Mar-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	nfsbxyt 1974*	Closed form of nfsbxy 1973. (Contributed by Jim Kingdon, 9-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbco2vlem 1975*	This is a version of sbco2 1996 where 𝑧 is distinct from 𝑥 and from 𝑦. It is a lemma on the way to proving sbco2v 1979 which only requires that 𝑧 and 𝑥 be distinct. (Contributed by Jim Kingdon, 25-Dec-2017.) Remove one disjoint variable condition. (Revised by Jim Kingdon, 3-Feb-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2vh 1976*	This is a version of sbco2 1996 where 𝑧 is distinct from 𝑥. (Contributed by Jim Kingdon, 12-Feb-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	nfsb 1977*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	nfsbv 1978*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 1977 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	sbco2v 1979*	Version of sbco2 1996 with disjoint variable conditions. (Contributed by Wolf Lammen, 29-Apr-2023.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	hbsb 1980*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	equsb3lem 1981*	Lemma for equsb3 1982. (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	equsb3 1982*	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	sbn 1983	Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
Theorem	sbim 1984	Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbor 1985	Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sban 1986	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	sbrim 1987	Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblim 1988	Substitution with a variable not free in consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	sb3an 1989	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
Theorem	sbbi 1990	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sblbis 1991	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓))
Theorem	sbrbis 1992	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbrbif 1993	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	sbco2yz 1994*	This is a version of sbco2 1996 where 𝑧 is distinct from 𝑦. It is a lemma on the way to proving sbco2 1996 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2h 1995	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2 1996	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2d 1997	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco2vd 1998*	Version of sbco2d 1997 with a distinct variable constraint between 𝑥 and 𝑧. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco 1999	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco3v 2000*	Version of sbco3 2005 with a distinct variable constraint between 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)