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	aaan 1601	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 1602	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 1603	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 1604	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 1605	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1604. (Contributed by DAW, 13-Feb-2017.)
|- ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.23bi 1606	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ph -> ps )   =>    |- ( ph -> ps )
Theorem	exlimih 1607	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 1608	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 1609	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1610 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 1610	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 1611	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 1612*	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 1612 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 1613	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 1614	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( E. x ph -> E. x ps )
Theorem	2eximi 1615	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 1616	Inference associated with eximi 1614. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	alinexa 1617	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	exbi 1618	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 1619	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 1620	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 1621	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 1622	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdd 1623	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 1624	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 1625	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 1626	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 1627	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 1628	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 1629	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 1630	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 1631	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 1632	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 1633	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1659. (Contributed by Jim Kingdon, 2-Jun-2018.)
|- ( A. xDECID ph -> ( A. x ph <-> -. E. x -. ph ) )
Theorem	19.29 1634	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 1635	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 1636	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 1637	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 1638	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 1639	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 1640	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 1641	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 1642	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 1643	The antecedent provides a condition implying the converse of 19.33 1498. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1644 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 1644	Converse of 19.33 1498 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 1643 (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 1645	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 1646	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 1647	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 1648	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 1649	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 1650	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 1651	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 1652	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 1653	Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1638, 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 1654	Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1638, 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 1655	A closed version of one direction of 19.9 1658. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )
Theorem	19.9t 1656	A closed version of 19.9 1658. (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 1657	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 1658	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 1659	One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1633. (Contributed by Jim Kingdon, 2-Jul-2018.)
|- ( A. x ph -> -. E. x -. ph )
Theorem	exnalim 1660	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 1661	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 1662	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 1663	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 1664	If x is not free in ph, it is not free in -. ph. This theorem doesn't use ax6b 1665 compared to hbnt 1667. (Contributed by GD, 27-Jan-2018.)
|- ( ph -> A. x ph )   =>    |- ( -. ph -> A. x -. ph )
Theorem	ax6b 1665	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 1666	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 1667	Closed theorem version of bound-variable hypothesis builder hbn 1668. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
Theorem	hbn 1668	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 1669	Deduction form of bound-variable hypothesis builder hbn 1668. (Contributed by NM, 3-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( -. ps -> A. x -. ps ) )
Theorem	nfnt 1670	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 1671	Deduction associated with nfnt 1670. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x -. ps )
Theorem	nfn 1672	Inference associated with nfnt 1670. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x -. ph
Theorem	nfdc 1673	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 1674	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 1675	A deduction version of one direction of 19.9 1658. (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 1676	A deduction version of one direction of 19.9 1658. This is an older variation of this theorem; new proofs should use 19.9d 1675. (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 1677	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 1678	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 1679	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 1680	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 1681	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 1682	An alternate definition of df-nf 1475, 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 1683	An alternate definition of df-nf 1475. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( F/ x ph <-> A. x ( E. x ph -> ph ) )
Theorem	nf4dc 1684	Variable x is effectively not free in ph iff ph is always true or always false, given a decidability condition. The reverse direction, nf4r 1685, 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 1685	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 1684. (Contributed by Jim Kingdon, 21-Jul-2018.)
|- ( ( A. x ph \/ A. x -. ph ) -> F/ x ph )
Theorem	19.36i 1686	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 1687	Closed form of 19.36i 1686. 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 1688	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 1689*	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 1690	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 1691	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 1692	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 1693	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 1694	One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if ph is decidable, as seen at 19.32dc 1693. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- F/ x ph   =>    |- ( ( ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
Theorem	19.31r 1695	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 1696	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 1697	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 1698	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 1699	Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1700 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 1700	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 ) )