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
Axiom	ax-13 1401	Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of the e. binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be. (Contributed by NM, 5-Aug-1993.)
|- (x = y -> (x e. z -> y e. z))
Axiom	ax-14 1402	Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of the e. binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. (Contributed by NM, 5-Aug-1993.)
|- (x = y -> (z e. x -> z e. y))
Theorem	hbequid 1403	Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (The proof uses only ax-5 1333, ax-8 1392, ax-12 1399, and ax-gen 1335. This shows that this can be proved without ax-9 1421, even though the theorem equid 1586 cannot be. A shorter proof using ax-9 1421 is obtainable from equid 1586 and hbth 1349.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.)
|- (x = x -> A.y x = x)
Theorem	axi12 1404	Proof that ax-i12 1395 follows from ax-bndl 1396. So that we can track which theorems rely on ax-bndl 1396, proofs should reference ax-i12 1395 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.)
|- (A.z z = x \/ (A.z z = y \/ A.z(x = y -> A.z x = y)))
Theorem	alequcom 1405	Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.)
|- (A.x x = y -> A.y y = x)
Theorem	alequcoms 1406	A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.)
|- (A.x x = y -> ph)   =>   |- (A.y y = x -> ph)
Theorem	nalequcoms 1407	A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.)
|- (-. A.x x = y -> ph)   =>   |- (-. A.y y = x -> ph)
Theorem	nfr 1408	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
|- ( F/xph -> (ph -> A.xph))
Theorem	nfri 1409	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   =>   |- (ph -> A.xph)
Theorem	nfrd 1410	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- (ph -> F/xps)   =>   |- (ph -> (ps -> A.xps))
Theorem	alimd 1411	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> A.xch))
Theorem	alrimi 1412	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	nfd 1413	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> F/xps)
Theorem	nfdh 1414	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- (ph -> F/xps)
Theorem	nfrimi 1415	Moving an antecedent outside F/. (Contributed by Jim Kingdon, 23-Mar-2018.)
|- F/xph   &   |- F/x(ph -> ps)   =>   |- (ph -> F/xps)
1.3.3  Axiom ax-17 - first use of the $d distinct variable statement
Axiom	ax-17 1416*	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.xph)
Theorem	a17d 1417*	ax-17 1416 with antecedent. (Contributed by NM, 1-Mar-2013.)
|- (ph -> (ps -> A.xps))
Theorem	nfv 1418*	If x is not present in ph, then x is not free in ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph
Theorem	nfvd 1419*	nfv 1418 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1474. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- (ph -> F/xps)
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1420	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 1397 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 1583, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- E.x x = y
Theorem	ax-9 1421	Derive ax-9 1421 from ax-i9 1420, the modified version for intuitionistic logic. Although ax-9 1421 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1420. (Contributed by NM, 3-Feb-2015.)
|- -. A.x -. x = y
Theorem	equidqe 1422	equid 1586 with some quantification and negation without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
|- -. A.y -. x = x
Theorem	ax4sp1 1423	A special case of ax-4 1397 without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.)
|- (A.y -. x = x -> -. x = x)
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1424	x is not free in A.xph. Axiom 7 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- (A.xph -> A.xA.xph)
Axiom	ax-i5r 1425	Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ((A.xph -> A.xps) -> A.x(A.xph -> ps))
1.3.6  Predicate calculus including ax-4, without distinct variables
Theorem	spi 1426	Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.)
|- A.xph   =>   |- ph
Theorem	sps 1427	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   =>   |- (A.xph -> ps)
Theorem	spsd 1428	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.xps -> ch))
Theorem	nfbidf 1429	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> ( F/xps <-> F/xch))
Theorem	hba1 1430	x is not free in A.xph. 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.xph -> A.xA.xph)
Theorem	nfa1 1431	x is not free in A.xph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xA.xph
Theorem	a5i 1432	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
|- (A.xph -> ps)   =>   |- (A.xph -> A.xps)
Theorem	nfnf1 1433	x is not free in F/xph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/x F/xph
Theorem	hbim 1434	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.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	hbor 1435	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.xph)   &   |- (ps -> A.xps)   =>   |- ((ph \/ ps) -> A.x(ph \/ ps))
Theorem	hban 1436	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.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))
Theorem	hbbi 1437	If x is not free in ph and ps, it is not free in (ph <-> ps). (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph <-> ps) -> A.x(ph <-> ps))
Theorem	hb3or 1438	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.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph \/ ps \/ ch) -> A.x(ph \/ ps \/ ch))
Theorem	hb3an 1439	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.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))
Theorem	hba2 1440	Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- (A.yA.xph -> A.xA.yA.xph)
Theorem	hbia1 1441	Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))
Theorem	19.3h 1442	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.xph)   =>   |- (A.xph <-> ph)
Theorem	19.3 1443	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/xph   =>   |- (A.xph <-> ph)
Theorem	19.16 1444	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/xph   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 1445	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/xps   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.21h 1446	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 1472 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.21bi 1447	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 1448	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	19.27h 1449	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (ps -> A.xps)   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.27 1450	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xps   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28h 1451	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xph)   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.28 1452	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/xph   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	nfan1 1453	A closed form of nfan 1454. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/xph   &   |- (ph -> F/xps)   =>   |- F/x(ph /\ ps)
Theorem	nfan 1454	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/xph   &   |- F/xps   =>   |- F/x(ph /\ ps)
Theorem	nf3an 1455	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/xph   &   |- F/xps   &   |- F/xch   =>   |- F/x(ph /\ ps /\ ch)
Theorem	nford 1456	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/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps \/ ch))
Theorem	nfand 1457	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/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps /\ ch))
Theorem	nf3and 1458	Deduction form of bound-variable hypothesis builder nf3an 1455. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   &   |- (ph -> F/xth)   =>   |- (ph -> F/x(ps /\ ch /\ th))
Theorem	hbim1 1459	A closed form of hbim 1434. (Contributed by NM, 5-Aug-1993.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	nfim1 1460	A closed form of nfim 1461. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/xph   &   |- (ph -> F/xps)   =>   |- F/x(ph -> ps)
Theorem	nfim 1461	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/xph   &   |- F/xps   =>   |- F/x(ph -> ps)
Theorem	hbimd 1462	Deduction form of bound-variable hypothesis builder hbim 1434. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps -> ch) -> A.x(ps -> ch)))
Theorem	nfor 1463	If x is not free in ph and ps, it is not free in (ph \/ ps). (Contributed by Jim Kingdon, 11-Mar-2018.)
|- F/xph   &   |- F/xps   =>   |- F/x(ph \/ ps)
Theorem	hbbid 1464	Deduction form of bound-variable hypothesis builder hbbi 1437. (Contributed by NM, 1-Jan-2002.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> A.xps))   &   |- (ph -> (ch -> A.xch))   =>   |- (ph -> ((ps <-> ch) -> A.x(ps <-> ch)))
Theorem	nfal 1465	If x is not free in ph, it is not free in A.yph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/xph   =>   |- F/xA.yph
Theorem	nfnf 1466	If x is not free in ph, it is not free in F/yph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/xph   =>   |- F/x F/yph
Theorem	nfalt 1467	Closed form of nfal 1465. (Contributed by Jim Kingdon, 11-May-2018.)
|- (A.y F/xph -> F/xA.yph)
Theorem	nfa2 1468	Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xA.yA.xph
Theorem	nfia1 1469	Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/x(A.xph -> A.xps)
Theorem	19.21ht 1470	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.)
|- (A.x(ph -> A.xph) -> (A.x(ph -> ps) <-> (ph -> A.xps)))
Theorem	19.21t 1471	Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
|- ( F/xph -> (A.x(ph -> ps) <-> (ph -> A.xps)))
Theorem	19.21 1472	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/xph   =>   |- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	stdpc5 1473	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis F/xph 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 1587. 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/xph   =>   |- (A.x(ph -> ps) -> (ph -> A.xps))
Theorem	nfimd 1474	If in a context x is not free in ps and ch, it is not free in (ps -> ch). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps -> ch))
Theorem	aaanh 1475	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	aaan 1476	Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
|- F/yph   &   |- F/xps   =>   |- (A.xA.y(ph /\ ps) <-> (A.xph /\ A.yps))
Theorem	nfbid 1477	If in a context x is not free in ps and ch, it is not free in (ps <-> ch). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.)
|- (ph -> F/xps)   &   |- (ph -> F/xch)   =>   |- (ph -> F/x(ps <-> ch))
Theorem	nfbi 1478	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/xph   &   |- F/xps   =>   |- F/x(ph <-> ps)
1.3.7  The existential quantifier
Theorem	19.8a 1479	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.)
|- (ph -> E.xph)
Theorem	19.23bi 1480	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (E.xph -> ps)   =>   |- (ph -> ps)
Theorem	exlimih 1481	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.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exlimi 1482	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xps   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exlimd2 1483	Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1484 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
|- (ph -> A.xph)   &   |- (ph -> (ch -> A.xch))   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	exlimdh 1484	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	exlimd 1485	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/xph   &   |- F/xch   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	exlimiv 1486*	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.xph(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 1486 to arrive at (E.xph -> ps). Finally, we separately prove E.xph and detach it with modus ponens ax-mp 7 to arrive at the final theorem ps. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)
|- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	exim 1487	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.xph -> E.xps))
Theorem	eximi 1488	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
|- (ph -> ps)   =>   |- (E.xph -> E.xps)
Theorem	2eximi 1489	Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
|- (ph -> ps)   =>   |- (E.xE.yph -> E.xE.yps)
Theorem	eximii 1490	Inference associated with eximi 1488. (Contributed by BJ, 3-Feb-2018.)
|- E.xph   &   |- (ph -> ps)   =>   |- E.xps
Theorem	alinexa 1491	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- (A.x(ph -> -. ps) <-> -. E.x(ph /\ ps))
Theorem	exbi 1492	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
Theorem	exbii 1493	Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
|- (ph <-> ps)   =>   |- (E.xph <-> E.xps)
Theorem	2exbii 1494	Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
|- (ph <-> ps)   =>   |- (E.xE.yph <-> E.xE.yps)
Theorem	3exbii 1495	Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
|- (ph <-> ps)   =>   |- (E.xE.yE.zph <-> E.xE.yE.zps)
Theorem	exancom 1496	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	alrimdd 1497	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- (ph -> F/xps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	alrimd 1498	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- F/xps   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	eximdh 1499	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	eximd 1500	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/xph   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))