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	nf3and 1501	Deduction form of bound-variable hypothesis builder nf3an 1498. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝜃)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	hbim1 1502	A closed form of hbim 1477. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	nfim1 1503	A closed form of nfim 1504. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfim 1504	If 𝑥 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.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	hbimd 1505	Deduction form of bound-variable hypothesis builder hbim 1477. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
Theorem	nfor 1506	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∨ 𝜓). (Contributed by Jim Kingdon, 11-Mar-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)
Theorem	hbbid 1507	Deduction form of bound-variable hypothesis builder hbbi 1480. (Contributed by NM, 1-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜒) → ∀𝑥(𝜓 ↔ 𝜒)))
Theorem	nfal 1508	If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfnf 1509	If 𝑥 is not free in 𝜑, it is not free in Ⅎ𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝜑
Theorem	nfalt 1510	Closed form of nfal 1508. (Contributed by Jim Kingdon, 11-May-2018.)
⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑)
Theorem	nfa2 1511	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥∀𝑦∀𝑥𝜑
Theorem	nfia1 1512	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥(∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	19.21ht 1513	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21t 1514	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21 1515	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	stdpc5 1516	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 1630. 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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	nfimd 1517	If in a context 𝑥 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.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
Theorem	aaanh 1518	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	aaan 1519	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	nfbid 1520	If in a context 𝑥 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.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))
Theorem	nfbi 1521	If 𝑥 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.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)
1.3.7  The existential quantifier
Theorem	19.8a 1522	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.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.23bi 1523	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	exlimih 1524	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimi 1525	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimd2 1526	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1527 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimdh 1527	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimd 1528	Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimiv 1529*	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 𝑥 exists satisfying a wff, i.e. ∃𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 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 𝑥) 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 𝑥. Then we apply exlimiv 1529 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 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.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exim 1530	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	eximi 1531	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	2eximi 1532	Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)
Theorem	eximii 1533	Inference associated with eximi 1531. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	alinexa 1534	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	exbi 1535	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	exbii 1536	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Theorem	2exbii 1537	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)
Theorem	3exbii 1538	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)
Theorem	exancom 1539	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
Theorem	alrimdd 1540	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 1541	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximdh 1542	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	eximd 1543	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	nexd 1544	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)
Theorem	exbidh 1545	Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	albid 1546	Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Theorem	exbid 1547	Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))
Theorem	exsimpl 1548	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑)
Theorem	exsimpr 1549	Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓)
Theorem	alexdc 1550	Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1576. (Contributed by Jim Kingdon, 2-Jun-2018.)
⊢ (∀𝑥DECID 𝜑 → (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑))
Theorem	19.29 1551	Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r 1552	Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
Theorem	19.29r2 1553	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.29x 1554	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓))
Theorem	19.35-1 1555	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.)
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
Theorem	19.35i 1556	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ ∃𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∃𝑥𝜓)
Theorem	19.25 1557	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓))
Theorem	19.30dc 1558	Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (DECID ∃𝑥𝜓 → (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)))
Theorem	19.43 1559	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))
Theorem	19.33b2 1560	The antecedent provides a condition implying the converse of 19.33 1413. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1561 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.)
⊢ ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Theorem	19.33bdc 1561	Converse of 19.33 1413 given ¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) 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 1560 (Contributed by Jim Kingdon, 23-Apr-2018.)
⊢ (DECID ∃𝑥𝜑 → (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓))))
Theorem	19.40 1562	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
Theorem	19.40-2 1563	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑥∃𝑦𝜓))
Theorem	exintrbi 1564	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	exintr 1565	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
Theorem	alsyl 1566	Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒))
Theorem	hbex 1567	If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
Theorem	nfex 1568	If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	19.2 1569	Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)
⊢ (∀𝑥𝜑 → ∃𝑦𝜑)
Theorem	i19.24 1570	Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1555, 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.)
⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))    ⇒   ⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	i19.39 1571	Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1555, 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.)
⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))    ⇒   ⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓))
Theorem	19.9ht 1572	A closed version of one direction of 19.9 1575. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑))
Theorem	19.9t 1573	A closed version of 19.9 1575. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.)
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 ↔ 𝜑))
Theorem	19.9h 1574	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.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	19.9 1575	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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	alexim 1576	One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1550. (Contributed by Jim Kingdon, 2-Jul-2018.)
⊢ (∀𝑥𝜑 → ¬ ∃𝑥 ¬ 𝜑)
Theorem	exnalim 1577	One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)
Theorem	exanaliim 1578	A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) → ¬ ∀𝑥(𝜑 → 𝜓))
Theorem	alexnim 1579	A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)
⊢ (∀𝑥∃𝑦 ¬ 𝜑 → ¬ ∃𝑥∀𝑦𝜑)
Theorem	ax6blem 1580	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. This theorem doesn't use ax6b 1581 compared to hbnt 1583. (Contributed by GD, 27-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	ax6b 1581	Quantified Negation. Axiom C5-2 of [Monk2] p. 113. (Contributed by GD, 27-Jan-2018.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hbn1 1582	𝑥 is not free in ¬ ∀𝑥𝜑. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
Theorem	hbnt 1583	Closed theorem version of bound-variable hypothesis builder hbn 1584. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	hbn 1584	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	hbnd 1585	Deduction form of bound-variable hypothesis builder hbn 1584. (Contributed by NM, 3-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓))
Theorem	nfnt 1586	If 𝑥 is not free in 𝜑, then it is not free in ¬ 𝜑. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
Theorem	nfnd 1587	Deduction associated with nfnt 1586. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Theorem	nfn 1588	Inference associated with nfnt 1586. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 ¬ 𝜑
Theorem	nfdc 1589	If 𝑥 is not free in 𝜑, it is not free in DECID 𝜑. (Contributed by Jim Kingdon, 11-Mar-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥DECID 𝜑
Theorem	modal-5 1590	The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
⊢ (¬ ∀𝑥 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)
Theorem	19.9d 1591	A deduction version of one direction of 19.9 1575. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜓 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	19.9hd 1592	A deduction version of one direction of 19.9 1575. This is an older variation of this theorem; new proofs should use 19.9d 1591. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜓 → (𝜑 → ∀𝑥𝜑))    ⇒   ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑))
Theorem	excomim 1593	One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
Theorem	excom 1594	Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)
Theorem	19.12 1595	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	19.19 1596	Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓))
Theorem	19.21-2 1597	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	nf2 1598	An alternate definition of df-nf 1390, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
Theorem	nf3 1599	An alternate definition of df-nf 1390. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	nf4dc 1600	Variable 𝑥 is effectively not free in 𝜑 iff 𝜑 is always true or always false, given a decidability condition. The reverse direction, nf4r 1601, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.)
⊢ (DECID ∃𝑥𝜑 → (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑)))