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	19.36aiv 1901*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.41v 1902*	Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.41vv 1903*	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
Theorem	19.41vvv 1904*	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.41vvvv 1905*	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓))
Theorem	19.42v 1906*	Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	spvv 1907*	Version of spv 1860 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarvv 1908*	Version of chvarv 1937 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	exdistr 1909*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	exdistrv 1910*	Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1902 and 19.42v 1906. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1932. (Contributed by BJ, 30-Sep-2022.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	19.42vv 1911*	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	19.42vvv 1912*	Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓))
Theorem	19.42vvvv 1913*	Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑤∃𝑥∃𝑦∃𝑧𝜓))
Theorem	exdistr2 1914*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓))
Theorem	3exdistr 1915*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒)))
Theorem	4exdistr 1916*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃))))
Theorem	cbvalv 1917*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv 1918*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvalvw 1919*	Change bound variable. See cbvalv 1917 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1448. (Revised by Gino Giotto, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexvw 1920*	Change bound variable. See cbvexv 1918 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1448. (Revised by Gino Giotto, 25-Aug-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbval2 1921*	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 1922*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbval2v 1923*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2v 1924*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvald 1925*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2017. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdh 1926*	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 2017. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvexd 1927*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2017. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldva 1928*	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 1929*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvex4v 1930*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	eean 1931	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeanv 1932*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeeanv 1933*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))
Theorem	ee4anv 1934*	Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓))
Theorem	ee8anv 1935*	Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ∧ ∃𝑣∃𝑢∃𝑡∃𝑠𝜓))
Theorem	nexdv 1936*	Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	chvarv 1937*	Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
1.4.5  More substitution theorems
Theorem	hbs1 1938*	𝑥 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 1939*	𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sbhb 1940*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by NM, 29-May-2009.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))
Theorem	hbsbv 1941*	This is a version of hbsb 1949 with an extra distinct variable constraint, on 𝑧 and 𝑥. (Contributed by Jim Kingdon, 25-Dec-2017.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfsbxy 1942*	Similar to hbsb 1949 but with an extra distinct variable constraint, on 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Mar-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	nfsbxyt 1943*	Closed form of nfsbxy 1942. (Contributed by Jim Kingdon, 9-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbco2vlem 1944*	This is a version of sbco2 1965 where 𝑧 is distinct from 𝑥 and from 𝑦. It is a lemma on the way to proving sbco2v 1948 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 1945*	This is a version of sbco2 1965 where 𝑧 is distinct from 𝑥. (Contributed by Jim Kingdon, 12-Feb-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	nfsb 1946*	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 1947*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is distinct from 𝑥 and 𝑦. Version of nfsb 1946 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 Gino Giotto, 25-Aug-2024.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	sbco2v 1948*	Version of sbco2 1965 with disjoint variable conditions. (Contributed by Wolf Lammen, 29-Apr-2023.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	hbsb 1949*	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 1950*	Lemma for equsb3 1951. (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	equsb3 1951*	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
Theorem	sbn 1952	Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
Theorem	sbim 1953	Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbor 1954	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 1955	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 1956	Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblim 1957	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 1958	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
Theorem	sbbi 1959	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sblbis 1960	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓))
Theorem	sbrbis 1961	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbrbif 1962	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	sbco2yz 1963*	This is a version of sbco2 1965 where 𝑧 is distinct from 𝑦. It is a lemma on the way to proving sbco2 1965 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2h 1964	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2 1965	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2d 1966	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco2vd 1967*	Version of sbco2d 1966 with a distinct variable constraint between 𝑥 and 𝑧. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco 1968	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco3v 1969*	Version of sbco3 1974 with a distinct variable constraint between 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcocom 1970	Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	sbcomv 1971*	Version of sbcom 1975 with a distinct variable constraint between 𝑥 and 𝑧. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbcomxyyz 1972*	Version of sbcom 1975 with distinct variable constraints between 𝑥 and 𝑦, and 𝑦 and 𝑧. (Contributed by Jim Kingdon, 21-Mar-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbco3xzyz 1973*	Version of sbco3 1974 with distinct variable constraints between 𝑥 and 𝑧, and 𝑦 and 𝑧. Lemma for proving sbco3 1974. (Contributed by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbco3 1974	A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcom 1975	A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	nfsbt 1976*	Closed form of nfsb 1946. (Contributed by Jim Kingdon, 9-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfsbd 1977*	Deduction version of nfsb 1946. (Contributed by NM, 15-Feb-2013.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓)
Theorem	sb9v 1978*	Like sb9 1979 but with a distinct variable constraint between 𝑥 and 𝑦. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9 1979	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9i 1980	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sbnf2 1981*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	hbsbd 1982*	Deduction version of hbsb 1949. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → ∀𝑧[𝑦 / 𝑥]𝜓))
Theorem	2sb5 1983*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	2sb6 1984*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sbcom2v 1985*	Lemma for proving sbcom2 1987. It is the same as sbcom2 1987 but with additional distinct variable constraints on 𝑥 and 𝑦, and on 𝑤 and 𝑧. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbcom2v2 1986*	Lemma for proving sbcom2 1987. It is the same as sbcom2v 1985 but removes the distinct variable constraint on 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbcom2 1987*	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sb6a 1988*	Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	2sb5rf 1989*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → ∀𝑤𝜑)    ⇒   ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	2sb6rf 1990*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → ∀𝑤𝜑)    ⇒   ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	dfsb7 1991*	An alternate definition of proper substitution df-sb 1763. By introducing a dummy variable 𝑧 in the definiens, we are able to eliminate any distinct variable restrictions among the variables 𝑥, 𝑦, and 𝜑 of the definiendum. No distinct variable conflicts arise because 𝑧 effectively insulates 𝑥 from 𝑦. To achieve this, we use a chain of two substitutions in the form of sb5 1887, first 𝑧 for 𝑥 then 𝑦 for 𝑧. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1992 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7f 1992*	This version of dfsb7 1991 does not require that 𝜑 and 𝑧 be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1526, i.e., that does not have the concept of a variable not occurring in a formula. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7af 1993*	An alternate definition of proper substitution df-sb 1763. Similar to dfsb7a 1994 but does not require that 𝜑 and 𝑧 be distinct. Similar to sb7f 1992 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. (Contributed by Jim Kingdon, 5-Feb-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Theorem	dfsb7a 1994*	An alternate definition of proper substitution df-sb 1763. Similar to dfsb7 1991 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. For a version which only requires Ⅎ𝑧𝜑 rather than 𝑧 and 𝜑 being distinct, see sb7af 1993. (Contributed by Jim Kingdon, 5-Feb-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Theorem	sb10f 1995*	Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. (Contributed by NM, 9-May-2005.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑))
Theorem	sbid2v 1996*	An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbelx 1997*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbel2x 1998*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sbalyz 1999*	Move universal quantifier in and out of substitution. Identical to sbal 2000 except that it has an additional distinct variable constraint on 𝑦 and 𝑧. (Contributed by Jim Kingdon, 29-Dec-2017.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbal 2000*	Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)