P. 15 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1401-1500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	a17d 1401*	ax-17 1400 with antecedent. (Contributed by NM, 1-Mar-2013.)
⊢ (φ → (ψ → ∀xψ))
Theorem	nfv 1402*	If x is not present in φ, then x is not free in φ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ
Theorem	nfvd 1403*	nfv 1402 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1459. (Contributed by Mario Carneiro, 6-Oct-2016.)
⊢ (φ → Ⅎxψ)
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1404	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 1381 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 1568, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ ∃x x = y
Theorem	ax-9 1405	Derive ax-9 1405 from ax-i9 1404, the modified version for intuitionistic logic. Although ax-9 1405 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1404. (Contributed by NM, 3-Feb-2015.)
⊢ ¬ ∀x ¬ x = y
Theorem	equidqe 1406	equid 1571 with some quantification and negation without using ax-4 1381 or ax-17 1400. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
⊢ ¬ ∀y ¬ x = x
Theorem	equidqeOLD 1407	Obsolete proof of equidqe 1406 as of 27-Feb-2014. (Contributed by NM, 13-Jan-2011.)
⊢ ¬ ∀y ¬ x = x
Theorem	ax4sp1 1408	A special case of ax-4 1381 without using ax-4 1381 or ax-17 1400. (Contributed by NM, 13-Jan-2011.)
⊢ (∀y ¬ x = x → ¬ x = x)
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1409	x is not free in ∀xφ. Axiom 7 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ (∀xφ → ∀x∀xφ)
Axiom	ax-i5r 1410	Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ψ))
1.3.6  Predicate calculus including ax-4, without distinct variables
Theorem	spi 1411	Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
⊢ ∀xφ    ⇒   ⊢ φ
Theorem	sps 1412	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
Theorem	spsd 1413	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀xψ → χ))
Theorem	nfbidf 1414	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (Ⅎxψ ↔ Ⅎxχ))
Theorem	hba1 1415	x is not free in ∀xφ. 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.)
⊢ (∀xφ → ∀x∀xφ)
Theorem	nfa1 1416	x is not free in ∀xφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎx∀xφ
Theorem	a5i 1417	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (∀xφ → ψ)    ⇒   ⊢ (∀xφ → ∀xψ)
Theorem	nfnf1 1418	x is not free in Ⅎxφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ ℲxℲxφ
Theorem	hbim 1419	If x is not free in φ and ψ, it is not free in (φ → ψ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
Theorem	hbor 1420	If x is not free in φ and ψ, it is not free in (φ ∨ ψ). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ∨ ψ) → ∀x(φ ∨ ψ))
Theorem	hban 1421	If x is not free in φ and ψ, it is not free in (φ ∧ ψ). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ))
Theorem	hbbi 1422	If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ ((φ ↔ ψ) → ∀x(φ ↔ ψ))
Theorem	hb3or 1423	If x is not free in φ, ψ, and χ, it is not free in (φ ∨ ψ ∨ χ). (Contributed by NM, 14-Sep-2003.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    ⇒   ⊢ ((φ ∨ ψ ∨ χ) → ∀x(φ ∨ ψ ∨ χ))
Theorem	hb3an 1424	If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ). (Contributed by NM, 14-Sep-2003.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (χ → ∀xχ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → ∀x(φ ∧ ψ ∧ χ))
Theorem	hba2 1425	Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
⊢ (∀y∀xφ → ∀x∀y∀xφ)
Theorem	hbia1 1426	Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
⊢ ((∀xφ → ∀xψ) → ∀x(∀xφ → ∀xψ))
Theorem	19.3h 1427	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.)
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀xφ ↔ φ)
Theorem	19.3 1428	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.)
⊢ Ⅎxφ    ⇒   ⊢ (∀xφ ↔ φ)
Theorem	19.16 1429	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ ↔ ψ) → (φ ↔ ∀xψ))
Theorem	19.17 1430	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ψ))
Theorem	19.21h 1431	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in φ." New proofs should use 19.21 1457 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
Theorem	19.21bi 1432	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xψ)    ⇒   ⊢ (φ → ψ)
Theorem	19.21bbi 1433	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
⊢ (φ → ∀x∀yψ)    ⇒   ⊢ (φ → ψ)
Theorem	19.27h 1434	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ))
Theorem	19.27 1435	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxψ    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (∀xφ ∧ ψ))
Theorem	19.28h 1436	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ))
Theorem	19.28 1437	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ ∧ ψ) ↔ (φ ∧ ∀xψ))
Theorem	nfan1 1438	A closed form of nfan 1439. (Contributed by Mario Carneiro, 3-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ Ⅎx(φ ∧ ψ)
Theorem	nfan 1439	If x is not free in φ and ψ, it is not free in (φ ∧ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ∧ ψ)
Theorem	nf3an 1440	If x is not free in φ, ψ, and χ, it is not free in (φ ∧ ψ ∧ χ). (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎxχ    ⇒   ⊢ Ⅎx(φ ∧ ψ ∧ χ)
Theorem	nford 1441	If in a context x is not free in ψ and χ, it is not free in (ψ ∨ χ). (Contributed by Jim Kingdon, 29-Oct-2019.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ ∨ χ))
Theorem	nfand 1442	If in a context x is not free in ψ and χ, it is not free in (ψ ∧ χ). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ ∧ χ))
Theorem	nf3and 1443	Deduction form of bound-variable hypothesis builder nf3an 1440. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → Ⅎxθ)    ⇒   ⊢ (φ → Ⅎx(ψ ∧ χ ∧ θ))
Theorem	hbim1 1444	A closed form of hbim 1419. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    ⇒   ⊢ ((φ → ψ) → ∀x(φ → ψ))
Theorem	nfim1 1445	A closed form of nfim 1446. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ Ⅎx(φ → ψ)
Theorem	nfim 1446	If x is not free in φ and ψ, it is not free in (φ → ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ → ψ)
Theorem	hbimd 1447	Deduction form of bound-variable hypothesis builder hbim 1419. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))
Theorem	nfor 1448	If x is not free in φ and ψ, it is not free in (φ ∨ ψ). (Contributed by Jim Kingdon, 11-Mar-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ∨ ψ)
Theorem	hbbid 1449	Deduction form of bound-variable hypothesis builder hbbi 1422. (Contributed by NM, 1-Jan-2002.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀xχ))    ⇒   ⊢ (φ → ((ψ ↔ χ) → ∀x(ψ ↔ χ)))
Theorem	nfal 1450	If x is not free in φ, it is not free in ∀yφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∀yφ
Theorem	nfnf 1451	If x is not free in φ, it is not free in Ⅎyφ. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎxφ    ⇒   ⊢ ℲxℲyφ
Theorem	nfalt 1452	Closed form of nfal 1450. (Contributed by Jim Kingdon, 11-May-2018.)
⊢ (∀yℲxφ → Ⅎx∀yφ)
Theorem	nfa2 1453	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎx∀y∀xφ
Theorem	nfia1 1454	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎx(∀xφ → ∀xψ)
Theorem	19.21ht 1455	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.)
⊢ (∀x(φ → ∀xφ) → (∀x(φ → ψ) ↔ (φ → ∀xψ)))
Theorem	19.21t 1456	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
⊢ (Ⅎxφ → (∀x(φ → ψ) ↔ (φ → ∀xψ)))
Theorem	19.21 1457	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in φ." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
Theorem	stdpc5 1458	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎxφ can be thought of as emulating "x is not free in φ." 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 1572. 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.)
⊢ Ⅎxφ    ⇒   ⊢ (∀x(φ → ψ) → (φ → ∀xψ))
Theorem	nfimd 1459	If in a context x is not free in ψ and χ, it is not free in (ψ → χ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ → χ))
Theorem	aaanh 1460	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ))
Theorem	aaan 1461	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (∀x∀y(φ ∧ ψ) ↔ (∀xφ ∧ ∀yψ))
Theorem	nfbid 1462	If in a context x is not free in ψ and χ, it is not free in (ψ ↔ χ). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎxχ)    ⇒   ⊢ (φ → Ⅎx(ψ ↔ χ))
Theorem	nfbi 1463	If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    ⇒   ⊢ Ⅎx(φ ↔ ψ)
1.3.7  The existential quantifier
Theorem	19.8a 1464	If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∃xφ)
Theorem	19.23bi 1465	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃xφ → ψ)    ⇒   ⊢ (φ → ψ)
Theorem	exlimih 1466	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (ψ → ∀xψ)    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	exlimi 1467	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxψ    &   ⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	exlimd2 1468	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1469 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	exlimdh 1469	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
⊢ (φ → ∀xφ)    &   ⊢ (χ → ∀xχ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	exlimd 1470	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.)
⊢ Ⅎxφ    &   ⊢ Ⅎxχ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	exlimiv 1471*	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. ∃xφ(x) where φ(x) has x free, then we can use φ( 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 φ (containing x) as an antecedent for the main part of the proof. We eventually arrive at (φ → ψ) where ψ is the theorem to be proved and does not contain x. Then we apply exlimiv 1471 to arrive at (∃xφ → ψ). Finally, we separately prove ∃xφ and detach it with modus ponens ax-mp 7 to arrive at the final theorem ψ. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)
⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	exim 1472	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))
Theorem	eximi 1473	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ∃xψ)
Theorem	2eximi 1474	Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (φ → ψ)    ⇒   ⊢ (∃x∃yφ → ∃x∃yψ)
Theorem	eximii 1475	Inference associated with eximi 1473. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃xφ    &   ⊢ (φ → ψ)    ⇒   ⊢ ∃xψ
Theorem	alinexa 1476	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀x(φ → ¬ ψ) ↔ ¬ ∃x(φ ∧ ψ))
Theorem	exbi 1477	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x(φ ↔ ψ) → (∃xφ ↔ ∃xψ))
Theorem	exbii 1478	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃xφ ↔ ∃xψ)
Theorem	2exbii 1479	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x∃yφ ↔ ∃x∃yψ)
Theorem	3exbii 1480	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃x∃y∃zφ ↔ ∃x∃y∃zψ)
Theorem	exancom 1481	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃x(φ ∧ ψ) ↔ ∃x(ψ ∧ φ))
Theorem	alrimdd 1482	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxψ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀xχ))
Theorem	alrimd 1483	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎxψ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀xχ))
Theorem	eximdh 1484	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → ∃xχ))
Theorem	eximd 1485	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → ∃xχ))
Theorem	nexd 1486	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃xψ)
Theorem	exbidh 1487	Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃xχ))
Theorem	albid 1488	Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ ↔ ∀xχ))
Theorem	exbid 1489	Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃xχ))
Theorem	exsimpl 1490	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃x(φ ∧ ψ) → ∃xφ)
Theorem	exsimpr 1491	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃x(φ ∧ ψ) → ∃xψ)
Theorem	alexdc 1492	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1518. (Contributed by Jim Kingdon, 2-Jun-2018.)
⊢ (∀xDECID φ → (∀xφ ↔ ¬ ∃x ¬ φ))
Theorem	19.29 1493	Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((∀xφ ∧ ∃xψ) → ∃x(φ ∧ ψ))
Theorem	19.29r 1494	Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ ((∃xφ ∧ ∀xψ) → ∃x(φ ∧ ψ))
Theorem	19.29r2 1495	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
⊢ ((∃x∃yφ ∧ ∀x∀yψ) → ∃x∃y(φ ∧ ψ))
Theorem	19.29x 1496	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
⊢ ((∃x∀yφ ∧ ∀x∃yψ) → ∃x∃y(φ ∧ ψ))
Theorem	19.35-1 1497	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.)
⊢ (∃x(φ → ψ) → (∀xφ → ∃xψ))
Theorem	19.35i 1498	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ∃xψ)
Theorem	19.25 1499	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (∀y∃x(φ → ψ) → (∃y∀xφ → ∃y∃xψ))
Theorem	19.30dc 1500	Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (DECID ∃xψ → (∀x(φ ∨ ψ) → (∀xφ ∨ ∃xψ)))