P. 16 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1501-1600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfrd 1501	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> ( ps -> A. x ps ) )
Theorem	alimd 1502	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	alrimi 1503	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	nfd 1504	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfdh 1505	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfrimi 1506	Moving an antecedent outside F/. (Contributed by Jim Kingdon, 23-Mar-2018.)
|- F/ x ph   &    |- F/ x ( ph -> ps )   =>    |- ( ph -> F/ x ps )
1.3.3  Axiom ax-17 - first use of the $d distinct variable statement
Axiom	ax-17 1507*	Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )
Theorem	a17d 1508*	ax-17 1507 with antecedent. (Contributed by NM, 1-Mar-2013.)
|- ( ph -> ( ps -> A. x ps ) )
Theorem	nfv 1509*	If x is not present in ph, then x is not free in ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph
Theorem	nfvd 1510*	nfv 1509 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1565. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- ( ph -> F/ x ps )
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1511	Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1488 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic"). In this form (not requiring that x and y be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) Another name for this theorem is a9e 1675, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- E. x x = y
Theorem	ax-9 1512	Derive ax-9 1512 from ax-i9 1511, the modified version for intuitionistic logic. Although ax-9 1512 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1511. (Contributed by NM, 3-Feb-2015.)
|- -. A. x -. x = y
Theorem	equidqe 1513	equid 1678 with some quantification and negation without using ax-4 1488 or ax-17 1507. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
|- -. A. y -. x = x
Theorem	ax4sp1 1514	A special case of ax-4 1488 without using ax-4 1488 or ax-17 1507. (Contributed by NM, 13-Jan-2011.)
|- ( A. y -. x = x -> -. x = x )
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1515	x is not free in A. x ph. One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( A. x ph -> A. x A. x ph )
Axiom	ax-i5r 1516	Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
1.3.6  Predicate calculus including ax-4, without distinct variables
Theorem	spi 1517	Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.)
|- A. x ph   =>    |- ph
Theorem	sps 1518	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	spsd 1519	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
Theorem	nfbidf 1520	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( F/ x ps <-> F/ x ch ) )
Theorem	hba1 1521	x is not free in A. x ph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> A. x A. x ph )
Theorem	nfa1 1522	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x A. x ph
Theorem	a5i 1523	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	nfnf1 1524	x is not free in F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/ x ph
Theorem	hbim 1525	If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	hbor 1526	If x is not free in ph and ps, it is not free in ( ph \/ ps ). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph \/ ps ) -> A. x ( ph \/ ps ) )
Theorem	hban 1527	If x is not free in ph and ps, it is not free in ( ph /\ ps ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hbbi 1528	If x is not free in ph and ps, it is not free in ( ph <-> ps ). (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph <-> ps ) -> A. x ( ph <-> ps ) )
Theorem	hb3or 1529	If x is not free in ph, ps, and ch, it is not free in ( ph \/ ps \/ ch ). (Contributed by NM, 14-Sep-2003.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph \/ ps \/ ch ) -> A. x ( ph \/ ps \/ ch ) )
Theorem	hb3an 1530	If x is not free in ph, ps, and ch, it is not free in ( ph /\ ps /\ ch ). (Contributed by NM, 14-Sep-2003.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	hba2 1531	Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- ( A. y A. x ph -> A. x A. y A. x ph )
Theorem	hbia1 1532	Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> A. x ps ) )
Theorem	19.3h 1533	A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 21-May-2007.)
|- ( ph -> A. x ph )   =>    |- ( A. x ph <-> ph )
Theorem	19.3 1534	A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   =>    |- ( A. x ph <-> ph )
Theorem	19.16 1535	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 1536	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 1537	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 1563 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 1538	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ps )   =>    |- ( ph -> ps )
Theorem	19.21bbi 1539	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> A. x A. y ps )   =>    |- ( ph -> ps )
Theorem	19.27h 1540	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 1541	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 1542	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 1543	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 1544	A closed form of nfan 1545. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1545	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 1546	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 1547	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 1548	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 1549	Deduction form of bound-variable hypothesis builder nf3an 1546. (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 1550	A closed form of hbim 1525. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1551	A closed form of nfim 1552. (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 1552	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 1553	Deduction form of bound-variable hypothesis builder hbim 1525. (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 1554	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 1555	Deduction form of bound-variable hypothesis builder hbbi 1528. (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 1556	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x A. y ph
Theorem	nfnf 1557	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 1558	Closed form of nfal 1556. (Contributed by Jim Kingdon, 11-May-2018.)
|- ( A. y F/ x ph -> F/ x A. y ph )
Theorem	nfa2 1559	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x A. y A. x ph
Theorem	nfia1 1560	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ( A. x ph -> A. x ps )
Theorem	19.21ht 1561	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 1562	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 1563	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 1564	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 1679. 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 1565	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 1566	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 1567	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 1568	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 1569	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 1570	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 1571	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1570. (Contributed by DAW, 13-Feb-2017.)
|- ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.23bi 1572	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ph -> ps )   =>    |- ( ph -> ps )
Theorem	exlimih 1573	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 1574	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 1575	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1576 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 1576	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 1577	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 1578*	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 1578 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 1579	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 1580	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( E. x ph -> E. x ps )
Theorem	2eximi 1581	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 1582	Inference associated with eximi 1580. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	alinexa 1583	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	exbi 1584	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 1585	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 1586	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 1587	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 1588	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdd 1589	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 1590	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 1591	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 1592	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 1593	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 1594	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 1595	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 1596	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 1597	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 1598	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 1599	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1625. (Contributed by Jim Kingdon, 2-Jun-2018.)
|- ( A. xDECID ph -> ( A. x ph <-> -. E. x -. ph ) )
Theorem	19.29 1600	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 ) )