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	axi12 1501	Proof that ax-i12 1494 follows from ax-bndl 1496. So that we can track which theorems rely on ax-bndl 1496, proofs should reference ax12or 1495 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.)
⊢ (∀𝑧 𝑧 = 𝑥 ∨ (∀𝑧 𝑧 = 𝑦 ∨ ∀𝑧(𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	alequcom 1502	Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	alequcoms 1503	A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	nalequcoms 1504	A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	nfr 1505	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	nfri 1506	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nfrd 1507	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	alimd 1508	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
Theorem	alrimi 1509	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∀𝑥𝜓)
Theorem	nfd 1510	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	nfdh 1511	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	nfrimi 1512	Moving an antecedent outside Ⅎ. (Contributed by Jim Kingdon, 23-Mar-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥(𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
1.3.3  Axiom ax-17 - first use of the $d distinct variable statement
Axiom	ax-17 1513*	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.)
⊢ (𝜑 → ∀𝑥𝜑)
Theorem	a17d 1514*	ax-17 1513 with antecedent. (Contributed by NM, 1-Mar-2013.)
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
Theorem	nfv 1515*	If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑
Theorem	nfvd 1516*	nfv 1515 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1572. (Contributed by Mario Carneiro, 6-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1517	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 1497 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 𝑥 and 𝑦 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 1683, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax-9 1518	Derive ax-9 1518 from ax-i9 1517, the modified version for intuitionistic logic. Although ax-9 1518 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1517. (Contributed by NM, 3-Feb-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	equidqe 1519	equid 1688 with some quantification and negation without using ax-4 1497 or ax-17 1513. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
⊢ ¬ ∀𝑦 ¬ 𝑥 = 𝑥
Theorem	ax4sp1 1520	A special case of ax-4 1497 without using ax-4 1497 or ax-17 1513. (Contributed by NM, 13-Jan-2011.)
⊢ (∀𝑦 ¬ 𝑥 = 𝑥 → ¬ 𝑥 = 𝑥)
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1521	𝑥 is not free in ∀𝑥𝜑. One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Axiom	ax-i5r 1522	Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → 𝜓))
1.3.6  Predicate calculus including ax-4, without distinct variables
Theorem	spi 1523	Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.)
⊢ ∀𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	sps 1524	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spsd 1525	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	nfbidf 1526	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒))
Theorem	hba1 1527	𝑥 is not free in ∀𝑥𝜑. 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.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	nfa1 1528	𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	axc4i 1529	Inference version of 19.21 1570. (Contributed by NM, 3-Jan-1993.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	a5i 1530	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	nfnf1 1531	𝑥 is not free in Ⅎ𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥Ⅎ𝑥𝜑
Theorem	hbim 1532	If 𝑥 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.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	hbor 1533	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∨ 𝜓). (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜓) → ∀𝑥(𝜑 ∨ 𝜓))
Theorem	hban 1534	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	hbbi 1535	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ↔ 𝜓) → ∀𝑥(𝜑 ↔ 𝜓))
Theorem	hb3or 1536	If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∨ 𝜓 ∨ 𝜒). (Contributed by NM, 14-Sep-2003.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → ∀𝑥(𝜑 ∨ 𝜓 ∨ 𝜒))
Theorem	hb3an 1537	If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by NM, 14-Sep-2003.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	hba2 1538	Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
⊢ (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦∀𝑥𝜑)
Theorem	hbia1 1539	Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	19.3h 1540	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.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.3 1541	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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ 𝜑)
Theorem	19.16 1542	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓))
Theorem	19.17 1543	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓))
Theorem	19.21h 1544	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑." New proofs should use 19.21 1570 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	19.21bi 1545	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.21bbi 1546	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → ∀𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	19.27h 1547	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.27 1548	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓))
Theorem	19.28h 1549	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	19.28 1550	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓))
Theorem	nfan1 1551	A closed form of nfan 1552. (Contributed by Mario Carneiro, 3-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	nfan 1552	If 𝑥 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.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	nf3an 1553	If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)
Theorem	nford 1554	If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 ∨ 𝜒). (Contributed by Jim Kingdon, 29-Oct-2019.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∨ 𝜒))
Theorem	nfand 1555	If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))
Theorem	nf3and 1556	Deduction form of bound-variable hypothesis builder nf3an 1553. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → Ⅎ𝑥𝜃)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	hbim1 1557	A closed form of hbim 1532. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	nfim1 1558	A closed form of nfim 1559. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	nfim 1559	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 1560	Deduction form of bound-variable hypothesis builder hbim 1532. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
Theorem	nfor 1561	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∨ 𝜓). (Contributed by Jim Kingdon, 11-Mar-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)
Theorem	hbbid 1562	Deduction form of bound-variable hypothesis builder hbbi 1535. (Contributed by NM, 1-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜒) → ∀𝑥(𝜓 ↔ 𝜒)))
Theorem	nfal 1563	If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1497. (Revised by Gino Giotto, 25-Aug-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfnf 1564	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 1565	Closed form of nfal 1563. (Contributed by Jim Kingdon, 11-May-2018.)
⊢ (∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥∀𝑦𝜑)
Theorem	nfa2 1566	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥∀𝑦∀𝑥𝜑
Theorem	nfia1 1567	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥(∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	19.21ht 1568	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21t 1569	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	19.21 1570	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 1571	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 1689. 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 1572	If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒))
Theorem	aaanh 1573	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	aaan 1574	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	nfbid 1575	If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ↔ 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒))
Theorem	nfbi 1576	If 𝑥 is not free in 𝜑 and 𝜓, then 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 1577	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.)
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	19.8ad 1578	If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1577. (Contributed by DAW, 13-Feb-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	19.23bi 1579	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃𝑥𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	exlimih 1580	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 1581	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimd2 1582	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1583 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimdh 1583	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	exlimd 1584	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 1585*	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 1585 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exim 1586	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	eximi 1587	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	2eximi 1588	Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓)
Theorem	eximii 1589	Inference associated with eximi 1587. (Contributed by BJ, 3-Feb-2018.)
⊢ ∃𝑥𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ ∃𝑥𝜓
Theorem	alinexa 1590	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓))
Theorem	exbi 1591	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
Theorem	exbii 1592	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Theorem	2exbii 1593	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)
Theorem	3exbii 1594	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)
Theorem	exancom 1595	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
Theorem	alrimdd 1596	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	alrimd 1597	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒))
Theorem	eximdh 1598	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	eximd 1599	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Theorem	nexd 1600	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ ∃𝑥𝜓)