P. 17 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1601-1700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfi 1601	Deduce that x is not free in ph from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> A. x ph )   =>    |- F/ x ph
Theorem	hbth 1602	No variable is (effectively) free in a theorem. This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form |- ( ph -> A. x ph ) from smaller formulas of this form. These are useful for constructing hypotheses that state " x is (effectively) not free in ph." (Contributed by NM, 11-May-1993.)
|- ph   =>    |- ( ph -> A. x ph )
Theorem	nfth 1603	No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ph   =>    |- F/ x ph
Theorem	nftru 1604	The true constant has no free variables. (This can also be proven in one step with nfv 1678, but this proof does not use ax-5 1675.) (Contributed by Mario Carneiro, 6-Oct-2016.)
|- F/ x T.
Theorem	nex 1605	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
|- -. ph   =>    |- -. E. x ph
Theorem	nfnth 1606	No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.)
|- -. ph   =>    |- F/ x ph
1.4.3  Axiom scheme ax-4 (Quantified Implication)
Axiom	ax-4 1607	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1608 for labelling consistency. It should be used only by alim 1608. (Contributed by NM, 21-May-2008.) (New usage is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	alim 1608	Restatement of Axiom ax-4 1607, for labelling consistency. It should be the only theorem using ax-4 1607. (Contributed by NM, 10-Jan-1993.)
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	alimi 1609	Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	2alimi 1610	Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
|- ( ph -> ps )   =>    |- ( A. x A. y ph -> A. x A. y ps )
Theorem	al2imi 1611	Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x ph -> ( A. x ps -> A. x ch ) )
Theorem	alanimi 1612	Variant of al2imi 1611 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( A. x ph /\ A. x ps ) -> A. x ch )
Theorem	alimdh 1613	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 4-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	albi 1614	Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.)
|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
Theorem	albii 1615	Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)
|- ( ph <-> ps )   =>    |- ( A. x ph <-> A. x ps )
Theorem	2albii 1616	Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)
|- ( ph <-> ps )   =>    |- ( A. x A. y ph <-> A. x A. y ps )
Theorem	alrimih 1617	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 9-Jan-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	hbxfrbi 1618	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2584 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ps )   &    |- ( ps -> A. x ps )   =>    |- ( ph -> A. x ph )
Theorem	nfbii 1619	Equality theorem for not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph <-> ps )   =>    |- ( F/ x ph <-> F/ x ps )
Theorem	nfxfr 1620	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph <-> ps )   &    |- F/ x ps   =>    |- F/ x ph
Theorem	nfxfrd 1621	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch -> F/ x ps )   =>    |- ( ch -> F/ x ph )
Theorem	alex 1622	Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
|- ( A. x ph <-> -. E. x -. ph )
Theorem	exnal 1623	Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( E. x -. ph <-> -. A. x ph )
Theorem	2nalexn 1624	Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. A. x A. y ph <-> E. x E. y -. ph )
Theorem	2exnaln 1625	Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ph <-> -. A. x A. y -. ph )
Theorem	2nexaln 1626	Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( -. E. x E. y ph <-> A. x A. y -. ph )
Theorem	aleximi 1627	A variant of al2imi 1611: instead of applying A. x quantifiers to the final implication, replace them with E. x. A shorter proof is possible using nfa1 1840, sps 1809 and eximd 1825, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x ph -> ( E. x ps -> E. x ch ) )
Theorem	exim 1628	Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
Theorem	eximOLD 1629	Obsolete proof of exim 1628 as of 4-Sep-2019. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
Theorem	eximi 1630	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
|- ( ph -> ps )   =>    |- ( E. x ph -> E. x ps )
Theorem	2eximi 1631	Inference adding two 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 1632	Inference associated with eximi 1630. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	aleximiOLD 1633	Obsolete proof of aleximi 1627 as of 4-Sep-2019. (Contributed by Wolf Lammen, 18-Aug-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x ph -> ( E. x ps -> E. x ch ) )
Theorem	19.38 1634	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 1847 and 19.23t 1851. (Revised by Wolf Lammen, 2-Jan-2018.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
Theorem	alinexa 1635	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	alexn 1636	A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.)
|- ( A. x E. y -. ph <-> -. E. x A. y ph )
Theorem	2exnexn 1637	Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.)
|- ( E. x A. y ph <-> -. A. x E. y -. ph )
Theorem	exbi 1638	Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
Theorem	exbii 1639	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 1640	Inference adding two 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 1641	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	exanali 1642	A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)
|- ( E. x ( ph /\ -. ps ) <-> -. A. x ( ph -> ps ) )
Theorem	exancom 1643	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdh 1644	Deduction from Theorem 19.21 of [Margaris] p. 90, see 19.21 1848. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	eximdh 1645	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	nexdh 1646	Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	albidh 1647	Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	exbidh 1648	Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )
Theorem	exsimpl 1649	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 1650	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	19.40 1651	Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.)
|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
Theorem	19.26 1652	Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )
Theorem	19.26-2 1653	Theorem 19.26 of [Margaris] p. 90 with two quantifiers. (Contributed by NM, 3-Feb-2005.)
|- ( A. x A. y ( ph /\ ps ) <-> ( A. x A. y ph /\ A. x A. y ps ) )
Theorem	19.26-3an 1654	Theorem 19.26 of [Margaris] p. 90 with triple conjunction. (Contributed by NM, 13-Sep-2011.)
|- ( A. x ( ph /\ ps /\ ch ) <-> ( A. x ph /\ A. x ps /\ A. x ch ) )
Theorem	19.29 1655	Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( A. x ph /\ E. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.29r 1656	Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
|- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.29r2 1657	Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
|- ( ( E. x E. y ph /\ A. x A. y ps ) -> E. x E. y ( ph /\ ps ) )
Theorem	19.29x 1658	Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
|- ( ( E. x A. y ph /\ A. x E. y ps ) -> E. x E. y ( ph /\ ps ) )
Theorem	19.35 1659	Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
Theorem	19.35OLD 1660	Obsolete proof of 19.35 1659 as of 4-Sep-2019. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
Theorem	19.35i 1661	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 21-Jun-1993.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> E. x ps )
Theorem	19.35ri 1662	Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( A. x ph -> E. x ps )   =>    |- E. x ( ph -> ps )
Theorem	19.25 1663	Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( A. y E. x ( ph -> ps ) -> ( E. y A. x ph -> E. y E. x ps ) )
Theorem	19.30 1664	Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) )
Theorem	19.43 1665	Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
Theorem	19.43OLD 1666	Obsolete proof of 19.43 1665 as of 3-May-2017. Leave this in for the example on the mmrecent.html page. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) )
Theorem	19.33 1667	Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
Theorem	19.33b 1668	The antecedent provides a condition implying the converse of 19.33 1667. Compare Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.)
|- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x ph \/ A. x ps ) ) )
Theorem	19.40-2 1669	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( E. x E. y ( ph /\ ps ) -> ( E. x E. y ph /\ E. x E. y ps ) )
Theorem	albiim 1670	Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( A. x ( ph <-> ps ) <-> ( A. x ( ph -> ps ) /\ A. x ( ps -> ph ) ) )
Theorem	2albiim 1671	Split a biconditional and distribute 2 quantifiers. (Contributed by NM, 3-Feb-2005.)
|- ( A. x A. y ( ph <-> ps ) <-> ( A. x A. y ( ph -> ps ) /\ A. x A. y ( ps -> ph ) ) )
Theorem	exintrbi 1672	Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
|- ( A. x ( ph -> ps ) -> ( E. x ph <-> E. x ( ph /\ ps ) ) )
Theorem	exintr 1673	Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ( ph /\ ps ) ) )
Theorem	alsyl 1674	Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ( ( A. x ( ph -> ps ) /\ A. x ( ps -> ch ) ) -> A. x ( ph -> ch ) )
1.4.4  Axiom scheme ax-5 (Distinctness) - first use of $d
Axiom	ax-5 1675*	Axiom of Distinctness. This axiom quantifies 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. (See comments in ax5ALT 2224 about the logical redundancy of ax-5 1675 in the presence of our obsolete axioms.) This axiom essentially says that if x does not occur in ph, i.e. ph does not depend on x in any way, then we can add the quantifier A. x to ph with no further assumptions. By sp 1803, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-1993.)
|- ( ph -> A. x ph )
Theorem	ax5d 1676*	ax-5 1675 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders. (Contributed by NM, 1-Mar-2013.)
|- ( ph -> ( ps -> A. x ps ) )
Theorem	ax5e 1677*	A rephrasing of ax-5 1675 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)
|- ( E. x ph -> ph )
Theorem	nfv 1678*	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 1679*	nfv 1678 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1859. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- ( ph -> F/ x ps )
Theorem	alimdv 1680*	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	eximdv 1681*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	2alimdv 1682*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x A. y ps -> A. x A. y ch ) )
Theorem	2eximdv 1683*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )
Theorem	albidv 1684*	Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	exbidv 1685*	Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. x ch ) )
Theorem	2albidv 1686*	Formula-building rule for 2 universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x A. y ps <-> A. x A. y ch ) )
Theorem	2exbidv 1687*	Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y ps <-> E. x E. y ch ) )
Theorem	3exbidv 1688*	Formula-building rule for 3 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y E. z ps <-> E. x E. y E. z ch ) )
Theorem	4exbidv 1689*	Formula-building rule for 4 existential quantifiers (deduction rule). (Contributed by NM, 3-Aug-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y E. z E. w ps <-> E. x E. y E. z E. w ch ) )
Theorem	alrimiv 1690*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 21-Jun-1993.)
|- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	alrimivv 1691*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
|- ( ph -> ps )   =>    |- ( ph -> A. x A. y ps )
Theorem	alrimdv 1692*	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	exlimiv 1693*	Inference from Theorem 19.23 of [Margaris] p. 90, see 19.23 1852. This inference, along with our many variants such as rexlimdv 2948, 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.appstate.edu/~hirstjl/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 (fictitious) 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 1693 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, 21-Jun-1993.) Remove dependencies on ax-6 1714 and ax-8 1764. (Revised by Wolf Lammen, 4-Dec-2017.)
|- ( ph -> ps )   =>    |- ( E. x ph -> ps )
Theorem	exlimivv 1694*	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
|- ( ph -> ps )   =>    |- ( E. x E. y ph -> ps )
Theorem	exlimdv 1695*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1714, ax-7 1734. (Revised by Wolf Lammen, 4-Dec-2017.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> ch ) )
Theorem	exlimdvv 1696*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x E. y ps -> ch ) )
Theorem	exlimddv 1697*	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ph -> E. x ps )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ( ph -> ch )
Theorem	nfdv 1698*	Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	2ax5 1699*	Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
|- ( ph -> A. x A. y ph )
1.4.5  Equality predicate (continued) The equality predicate was introduced above in wceq 1374 for use by df-tru 1377. See the comments in that section. In this section, we continue with the first "real" use of it.
Theorem	weq 1700	Extend wff definition to include atomic formulas using the equality predicate. (Instead of introducing weq 1700 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1374. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1700 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1374. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.)
wff x = y