P. 17 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1601-1700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2eximi 1601	Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)
Theorem	eximii 1602	Inference associated with eximi 1600. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	alinexa 1603	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	exbi 1604	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	exbii 1605	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Theorem	2exbii 1606	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)
Theorem	3exbii 1607	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)
Theorem	exancom 1608	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
Theorem	alrimdd 1609	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 1610	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximdh 1611	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	eximd 1612	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	nexd 1613	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	exbidh 1614	Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	albid 1615	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 1616	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exsimpl 1617	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
Theorem	exsimpr 1618	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓)
Theorem	alexdc 1619	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1645. (Contributed by Jim Kingdon, 2-Jun-2018.)
⊢ (∀𝑥DECID 𝜑 → (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑))
Theorem	19.29 1620	Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r 1621	Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r2 1622	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.29x 1623	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.35-1 1624	Forward direction of Theorem 19.35 of [Margaris] p. 90. The converse holds for classical logic but not (for all propositions) in intuitionistic logic. (Contributed by Mario Carneiro, 2-Feb-2015.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	19.35i 1625	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∃𝑥𝜓)
Theorem	19.25 1626	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓))
Theorem	19.30dc 1627	Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (DECID ∃𝑥𝜓 → (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)))
Theorem	19.43 1628	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.33b2 1629	The antecedent provides a condition implying the converse of 19.33 1484. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1630 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.)
⊢ ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Theorem	19.33bdc 1630	Converse of 19.33 1484 given ¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) and a decidability condition. Compare Theorem 19.33 of [Margaris] p. 90. For a version which does not require a decidability condition, see 19.33b2 1629 (Contributed by Jim Kingdon, 23-Apr-2018.)
⊢ (DECID ∃𝑥𝜑 → (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓))))
Theorem	19.40 1631	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
Theorem	19.40-2 1632	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	exintrbi 1633	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	exintr 1634	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	alsyl 1635	Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒))
Theorem	hbex 1636	If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
Theorem	nfex 1637	If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	19.2 1638	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)
⊢ (∀𝑥𝜑 → ∃𝑦𝜑)
Theorem	i19.24 1639	Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1624, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))    ⇒   ⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	i19.39 1640	Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1624, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))    ⇒   ⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.9ht 1641	A closed version of one direction of 19.9 1644. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑))
Theorem	19.9t 1642	A closed version of 19.9 1644. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.)
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 ↔ 𝜑))
Theorem	19.9h 1643	A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	19.9 1644	A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	alexim 1645	One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1619. (Contributed by Jim Kingdon, 2-Jul-2018.)
⊢ (∀𝑥𝜑 → ¬ ∃𝑥 ¬ 𝜑)
Theorem	exnalim 1646	One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	exanaliim 1647	A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) → ¬ ∀𝑥(𝜑 → 𝜓))
Theorem	alexnim 1648	A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∀𝑥∃𝑦 ¬ 𝜑 → ¬ ∃𝑥∀𝑦𝜑)
Theorem	nnal 1649	The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.)
⊢ (¬ ¬ ∀𝑥𝜑 → ∀𝑥 ¬ ¬ 𝜑)
Theorem	ax6blem 1650	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. This theorem doesn't use ax6b 1651 compared to hbnt 1653. (Contributed by GD, 27-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	ax6b 1651	Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by GD, 27-Jan-2018.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hbn1 1652	𝑥 is not free in ¬ ∀𝑥𝜑. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hbnt 1653	Closed theorem version of bound-variable hypothesis builder hbn 1654. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	hbn 1654	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	hbnd 1655	Deduction form of bound-variable hypothesis builder hbn 1654. (Contributed by NM, 3-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓))
Theorem	nfnt 1656	If 𝑥 is not free in 𝜑, then it is not free in ¬ 𝜑. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
Theorem	nfnd 1657	Deduction associated with nfnt 1656. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Theorem	nfn 1658	Inference associated with nfnt 1656. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 ¬ 𝜑
Theorem	nfdc 1659	If 𝑥 is not free in 𝜑, it is not free in DECID 𝜑. (Contributed by Jim Kingdon, 11-Mar-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥DECID 𝜑
Theorem	modal-5 1660	The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
⊢ (¬ ∀𝑥 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)
Theorem	19.9d 1661	A deduction version of one direction of 19.9 1644. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	19.9hd 1662	A deduction version of one direction of 19.9 1644. This is an older variation of this theorem; new proofs should use 19.9d 1661. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜓 → (𝜑 → ∀𝑥𝜑))    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	excomim 1663	One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	excom 1664	Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	19.12 1665	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	19.19 1666	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.21-2 1667	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	nf2 1668	An alternate definition of df-nf 1461, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	nf3 1669	An alternate definition of df-nf 1461. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	nf4dc 1670	Variable 𝑥 is effectively not free in 𝜑 iff 𝜑 is always true or always false, given a decidability condition. The reverse direction, nf4r 1671, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (DECID ∃𝑥𝜑 → (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑)))
Theorem	nf4r 1671	If 𝜑 is always true or always false, then variable 𝑥 is effectively not free in 𝜑. The converse holds given a decidability condition, as seen at nf4dc 1670. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ ((∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑) → Ⅎ𝑥𝜑)
Theorem	19.36i 1672	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ Ⅎ𝑥𝜓    &   ⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	19.36-1 1673	Closed form of 19.36i 1672. One direction of Theorem 19.36 of [Margaris] p. 90. The converse holds in classical logic, but does not hold (for all propositions) in intuitionistic logic. (Contributed by Jim Kingdon, 20-Jun-2018.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓))
Theorem	19.37-1 1674	One direction of Theorem 19.37 of [Margaris] p. 90. The converse holds in classical logic but not, in general, here. (Contributed by Jim Kingdon, 21-Jun-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓))
Theorem	19.37aiv 1675*	Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	19.38 1676	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	19.23t 1677	Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	19.23 1678	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	19.32dc 1679	Theorem 19.32 of [Margaris] p. 90, where 𝜑 is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (DECID 𝜑 → (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)))
Theorem	19.32r 1680	One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if 𝜑 is decidable, as seen at 19.32dc 1679. (Contributed by Jim Kingdon, 28-Jul-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓))
Theorem	19.31r 1681	One direction of Theorem 19.31 of [Margaris] p. 90. The converse holds in classical logic, but not intuitionistic logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ((∀𝑥𝜑 ∨ 𝜓) → ∀𝑥(𝜑 ∨ 𝜓))
Theorem	19.44 1682	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓))
Theorem	19.45 1683	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))
Theorem	19.34 1684	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓))
Theorem	19.41h 1685	Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1686 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.41 1686	Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
Theorem	19.42h 1687	Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1688 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	19.42 1688	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Theorem	excom13 1689	Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑧∃𝑦∃𝑥𝜑)
Theorem	exrot3 1690	Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑦∃𝑧∃𝑥𝜑)
Theorem	exrot4 1691	Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑧∃𝑤∃𝑥∃𝑦𝜑)
Theorem	nexr 1692	Inference from 19.8a 1590. (Contributed by Jeff Hankins, 26-Jul-2009.)
⊢ ¬ ∃𝑥𝜑    ⇒   ⊢ ¬ 𝜑
Theorem	exan 1693	Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃𝑥𝜑 ∧ 𝜓)    ⇒   ⊢ ∃𝑥(𝜑 ∧ 𝜓)
Theorem	hbexd 1694	Deduction form of bound-variable hypothesis builder hbex 1636. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (∃𝑦𝜓 → ∀𝑥∃𝑦𝜓))
Theorem	eeor 1695	Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
1.3.8  Equality theorems without distinct variables
Theorem	a9e 1696	At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1447 through ax-14 2151 and ax-17 1526, all axioms other than ax-9 1531 are believed to be theorems of free logic, although the system without ax-9 1531 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	a9ev 1697*	At least one individual exists. Weaker version of a9e 1696. (Contributed by NM, 3-Aug-2017.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax9o 1698	An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	spimfv 1699*	Specialization, using implicit substitution. Version of spim 1738 with a disjoint variable condition. See spimv 1811 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	chvarfv 1700*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 1757 with a disjoint variable condition. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓