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	19.16 1601	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) )
Theorem	19.17 1602	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ps   =>    |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) )
Theorem	19.21h 1603	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph". New proofs should use 19.21 1629 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	19.21bi 1604	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ps )   =>    |- ( ph -> ps )
Theorem	19.21bbi 1605	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> A. x A. y ps )   =>    |- ( ph -> ps )
Theorem	19.27h 1606	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.27 1607	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28h 1608	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	19.28 1609	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	nfan1 1610	A closed form of nfan 1611. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1611	If x is not free in ph and ps, it is not free in ( ph /\ ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nf3an 1612	If x is not free in ph, ps, and ch, it is not free in ( ph /\ ps /\ ch ). (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph /\ ps /\ ch )
Theorem	nford 1613	If in a context x is not free in ps and ch, it is not free in ( ps \/ ch ). (Contributed by Jim Kingdon, 29-Oct-2019.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps \/ ch ) )
Theorem	nfand 1614	If in a context x is not free in ps and ch, it is not free in ( ps /\ ch ). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps /\ ch ) )
Theorem	nf3and 1615	Deduction form of bound-variable hypothesis builder nf3an 1612. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/ x th )   =>    |- ( ph -> F/ x ( ps /\ ch /\ th ) )
Theorem	hbim1 1616	A closed form of hbim 1591. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1617	A closed form of nfim 1618. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfim 1618	If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	hbimd 1619	Deduction form of bound-variable hypothesis builder hbim 1591. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	nfor 1620	If x is not free in ph and ps, it is not free in ( ph \/ ps ). (Contributed by Jim Kingdon, 11-Mar-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph \/ ps )
Theorem	hbbid 1621	Deduction form of bound-variable hypothesis builder hbbi 1594. (Contributed by NM, 1-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps <-> ch ) -> A. x ( ps <-> ch ) ) )
Theorem	nfal 1622	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1556. (Revised by GG, 25-Aug-2024.)
|- F/ x ph   =>    |- F/ x A. y ph
Theorem	nfnf 1623	If x is not free in ph, it is not free in F/ y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x F/ y ph
Theorem	nfalt 1624	Closed form of nfal 1622. (Contributed by Jim Kingdon, 11-May-2018.)
|- ( A. y F/ x ph -> F/ x A. y ph )
Theorem	nfa2 1625	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x A. y A. x ph
Theorem	nfia1 1626	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ( A. x ph -> A. x ps )
Theorem	19.21ht 1627	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.)
|- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21t 1628	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	19.21 1629	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in ph". (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	stdpc5 1630	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis F/ x ph can be thought of as emulating " x is not free in ph". With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by nfequid 1748. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	nfimd 1631	If in a context x is not free in ps and ch, then it is not free in ( ps -> ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps -> ch ) )
Theorem	aaanh 1632	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- ( ph -> A. y ph )   &    |- ( ps -> A. x ps )   =>    |- ( A. x A. y ( ph /\ ps ) <-> ( A. x ph /\ A. y ps ) )
Theorem	aaan 1633	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( A. x A. y ( ph /\ ps ) <-> ( A. x ph /\ A. y ps ) )
Theorem	nfbid 1634	If in a context x is not free in ps and ch, then it is not free in ( ps <-> ch ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps <-> ch ) )
Theorem	nfbi 1635	If x is not free in ph and ps, then it is not free in ( ph <-> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph <-> ps )
1.3.7  The existential quantifier
Theorem	19.8a 1636	If a wff is true, then it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> E. x ph )
Theorem	19.8ad 1637	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1636. (Contributed by DAW, 13-Feb-2017.)
|- ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.23bi 1638	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ph -> ps )   =>    |- ( ph -> ps )
Theorem	exlimih 1639	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ps -> A. x ps )   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimi 1640	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ps   &    |- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimd2 1641	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1642 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdh 1642	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
|- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimd 1643	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimiv 1644*	Inference from Theorem 19.23 of [Margaris] p. 90. This inference, along with our many variants is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C. In essence, Rule C states that if we can prove that some element x exists satisfying a wff, i.e. E. x ph ( x ) where ph ( x ) has x free, then we can use ph ( C ) as a hypothesis for the proof where C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier. We cannot do this in Metamath directly. Instead, we use the original ph (containing x) as an antecedent for the main part of the proof. We eventually arrive at ( ph -> ps ) where ps is the theorem to be proved and does not contain x. Then we apply exlimiv 1644 to arrive at ( E. x ph -> ps ). Finally, we separately prove E. x ph and detach it with modus ponens ax-mp 5 to arrive at the final theorem ps. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)
|- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exim 1645	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
Theorem	eximi 1646	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( E. x ph -> E. x ps )
Theorem	2eximi 1647	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 1648	Inference associated with eximi 1646. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	alinexa 1649	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	exbi 1650	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 1651	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 1652	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 1653	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 1654	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdd 1655	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 1656	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 1657	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 1658	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 1659	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 1660	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 1661	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 1662	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 1663	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 1664	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 1665	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1691. (Contributed by Jim Kingdon, 2-Jun-2018.)
|- ( A. xDECID ph -> ( A. x ph <-> -. E. x -. ph ) )
Theorem	19.29 1666	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 1667	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 1668	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 1669	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 1670	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 1671	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 1672	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 1673	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 1674	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 1675	The antecedent provides a condition implying the converse of 19.33 1530. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1676 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 1676	Converse of 19.33 1530 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 1675 (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 1677	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 1678	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 1679	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 1680	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 1681	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 1682	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 1683	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 1684	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 1685	Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1670, 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 1686	Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1670, 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 1687	A closed version of one direction of 19.9 1690. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )
Theorem	19.9t 1688	A closed version of 19.9 1690. (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 1689	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 1690	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 1691	One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1665. (Contributed by Jim Kingdon, 2-Jul-2018.)
|- ( A. x ph -> -. E. x -. ph )
Theorem	exnalim 1692	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 1693	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 1694	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 1695	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 1696	If x is not free in ph, it is not free in -. ph. This theorem doesn't use ax6b 1697 compared to hbnt 1699. (Contributed by GD, 27-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	ax6b 1697	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 1698	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 1699	Closed theorem version of bound-variable hypothesis builder hbn 1700. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 1700	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 )