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.)
|- ( ph -> ps )   =>    |- ( E. x E. y ph -> E. x E. y ps )
Theorem	eximii 1602	Inference associated with eximi 1600. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	alinexa 1603	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	exbi 1604	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
Theorem	exbii 1605	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
|- ( ph <-> ps )   =>    |- ( E. x ph <-> E. x ps )
Theorem	2exbii 1606	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
|- ( ph <-> ps )   =>    |- ( E. x E. y ph <-> E. x E. y ps )
Theorem	3exbii 1607	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
|- ( ph <-> ps )   =>    |- ( E. x E. y E. z ph <-> E. x E. y E. z ps )
Theorem	exancom 1608	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdd 1609	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	alrimd 1610	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- F/ x ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	eximdh 1611	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	eximd 1612	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	nexd 1613	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	exbidh 1614	Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )
Theorem	albid 1615	Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	exbid 1616	Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )
Theorem	exsimpl 1617	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( E. x ( ph /\ ps ) -> E. x ph )
Theorem	exsimpr 1618	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
|- ( E. x ( ph /\ ps ) -> E. x ps )
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.)
|- ( A. xDECID ph -> ( A. x ph <-> -. E. x -. ph ) )
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.)
|- ( ( A. x ph /\ E. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.29r 1621	Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.29r2 1622	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
|- ( ( E. x E. y ph /\ A. x A. y ps ) -> E. x E. y ( ph /\ ps ) )
Theorem	19.29x 1623	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
|- ( ( E. x A. y ph /\ A. x E. y ps ) -> E. x E. y ( ph /\ ps ) )
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.)
|- ( E. x ( ph -> ps ) -> ( A. x ph -> E. x ps ) )
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.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> E. x ps )
Theorem	19.25 1626	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( A. y E. x ( ph -> ps ) -> ( E. y A. x ph -> E. y E. x ps ) )
Theorem	19.30dc 1627	Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- (DECID E. x ps -> ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) ) )
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.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
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.)
|- ( ( -. E. x ph \/ -. E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) )
Theorem	19.33bdc 1630	Converse of 19.33 1484 given -. ( E. x ph /\ E. x ps ) 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 E. x ph -> ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) ) )
Theorem	19.40 1631	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
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.)
|- ( E. x E. y ( ph /\ ps ) -> ( E. x E. y ph /\ E. x E. y ps ) )
Theorem	exintrbi 1633	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
|- ( A. x ( ph -> ps ) -> ( E. x ph <-> E. x ( ph /\ ps ) ) )
Theorem	exintr 1634	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ( ph /\ ps ) ) )
Theorem	alsyl 1635	Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ( ( A. x ( ph -> ps ) /\ A. x ( ps -> ch ) ) -> A. x ( ph -> ch ) )
Theorem	hbex 1636	If x is not free in ph, it is not free in E. y ph. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( ph -> A. x ph )   =>    |- ( E. y ph -> A. x E. y ph )
Theorem	nfex 1637	If x is not free in ph, it is not free in E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x E. y ph
Theorem	19.2 1638	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)
|- ( A. x ph -> E. y ph )
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.)
|- ( ( A. x ph -> E. x ps ) -> E. x ( ph -> ps ) )   =>    |- ( ( A. x ph -> A. x ps ) -> E. x ( ph -> ps ) )
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.)
|- ( ( A. x ph -> E. x ps ) -> E. x ( ph -> ps ) )   =>    |- ( ( E. x ph -> E. x ps ) -> E. x ( ph -> ps ) )
Theorem	19.9ht 1641	A closed version of one direction of 19.9 1644. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )
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.)
|- ( F/ x ph -> ( E. x ph <-> ph ) )
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.)
|- ( ph -> A. x ph )   =>    |- ( E. x ph <-> ph )
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.)
|- F/ x ph   =>    |- ( E. x ph <-> ph )
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.)
|- ( A. x ph -> -. E. x -. ph )
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.)
|- ( E. x -. ph -> -. A. x ph )
Theorem	exanaliim 1647	A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
|- ( E. x ( ph /\ -. ps ) -> -. A. x ( ph -> ps ) )
Theorem	alexnim 1648	A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)
|- ( A. x E. y -. ph -> -. E. x A. y ph )
Theorem	nnal 1649	The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.)
|- ( -. -. A. x ph -> A. x -. -. ph )
Theorem	ax6blem 1650	If x is not free in ph, it is not free in -. ph. This theorem doesn't use ax6b 1651 compared to hbnt 1653. (Contributed by GD, 27-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	ax6b 1651	Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by GD, 27-Jan-2018.)
|- ( -. A. x ph -> A. x -. A. x ph )
Theorem	hbn1 1652	x is not free in -. A. x ph. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
|- ( -. A. x ph -> A. x -. A. x ph )
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.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 1654	If x is not free in ph, it is not free in -. ph. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	hbnd 1655	Deduction form of bound-variable hypothesis builder hbn 1654. (Contributed by NM, 3-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( -. ps -> A. x -. ps ) )
Theorem	nfnt 1656	If x is not free in ph, then it is not free in -. ph. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
|- ( F/ x ph -> F/ x -. ph )
Theorem	nfnd 1657	Deduction associated with nfnt 1656. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfn 1658	Inference associated with nfnt 1656. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	nfdc 1659	If x is not free in ph, it is not free in DECID ph. (Contributed by Jim Kingdon, 11-Mar-2018.)
|- F/ x ph   =>    |- F/ xDECID ph
Theorem	modal-5 1660	The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
|- ( -. A. x -. ph -> A. x -. A. x -. ph )
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.)
|- ( ps -> F/ x ph )   =>    |- ( ps -> ( E. x ph -> ph ) )
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.)
|- ( ps -> A. x ps )   &    |- ( ps -> ( ph -> A. x ph ) )   =>    |- ( ps -> ( E. x ph -> ph ) )
Theorem	excomim 1663	One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( E. x E. y ph -> E. y E. x ph )
Theorem	excom 1664	Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( E. x E. y ph <-> E. y E. x ph )
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.)
|- ( E. x A. y ph -> A. y E. x ph )
Theorem	19.19 1666	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) )
Theorem	19.21-2 1667	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
|- F/ x ph   &    |- F/ y ph   =>    |- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )
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.)
|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
Theorem	nf3 1669	An alternate definition of df-nf 1461. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> A. x ( E. x ph -> ph ) )
Theorem	nf4dc 1670	Variable x is effectively not free in ph iff ph 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 E. x ph -> ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) ) )
Theorem	nf4r 1671	If ph is always true or always false, then variable x is effectively not free in ph. The converse holds given a decidability condition, as seen at nf4dc 1670. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( A. x ph \/ A. x -. ph ) -> F/ x ph )
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.)
|- F/ x ps   &    |- E. x ( ph -> ps )   =>    |- ( A. x ph -> ps )
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.)
|- F/ x ps   =>    |- ( E. x ( ph -> ps ) -> ( A. x ph -> ps ) )
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.)
|- F/ x ph   =>    |- ( E. x ( ph -> ps ) -> ( ph -> E. x ps ) )
Theorem	19.37aiv 1675*	Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- E. x ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.38 1676	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
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.)
|- ( F/ x ps -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23 1678	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.32dc 1679	Theorem 19.32 of [Margaris] p. 90, where ph is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
|- F/ x ph   =>    |- (DECID ph -> ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) )
Theorem	19.32r 1680	One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if ph is decidable, as seen at 19.32dc 1679. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- F/ x ph   =>    |- ( ( ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
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.)
|- F/ x ps   =>    |- ( ( A. x ph \/ ps ) -> A. x ( ph \/ ps ) )
Theorem	19.44 1682	Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ps   =>    |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45 1683	Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	19.34 1684	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ( A. x ph \/ E. x ps ) -> E. x ( ph \/ ps ) )
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.)
|- ( ps -> A. x ps )   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
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.)
|- F/ x ps   =>    |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
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.)
|- ( ph -> A. x ph )   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	19.42 1688	Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- F/ x ph   =>    |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	excom13 1689	Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y E. z ph <-> E. z E. y E. x ph )
Theorem	exrot3 1690	Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
|- ( E. x E. y E. z ph <-> E. y E. z E. x ph )
Theorem	exrot4 1691	Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y E. z E. w ph <-> E. z E. w E. x E. y ph )
Theorem	nexr 1692	Inference from 19.8a 1590. (Contributed by Jeff Hankins, 26-Jul-2009.)
|- -. E. x ph   =>    |- -. ph
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.)
|- ( E. x ph /\ ps )   =>    |- E. x ( ph /\ ps )
Theorem	hbexd 1694	Deduction form of bound-variable hypothesis builder hbex 1636. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> A. y ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( E. y ps -> A. x E. y ps ) )
Theorem	eeor 1695	Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x E. y ( ph \/ ps ) <-> ( E. x ph \/ E. y ps ) )
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.)
|- E. x x = y
Theorem	a9ev 1697*	At least one individual exists. Weaker version of a9e 1696. (Contributed by NM, 3-Aug-2017.)
|- E. x x = y
Theorem	ax9o 1698	An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
|- ( A. x ( x = y -> A. x ph ) -> ph )
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.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	chvarfv 1700*	Implicit substitution of y for x 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.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps