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	alnex 1601	Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
|- ( A. x -. ph <-> -. E. x ph )
Theorem	eximal 1602	A utility theorem. An interesting case is when the same formula is substituted for both ph and ps, since then both implications express a type of non-freeness. See also alimex 1639. (Contributed by BJ, 12-May-2019.)
|- ( ( E. x ph -> ps ) <-> ( -. ps -> A. x -. ph ) )
Syntax	wnf 1603	Extend wff definition to include the not-free predicate.
wff F/ x ph
Definition	df-nf 1604	Define the not-free predicate for wffs. This is read " x is not free in ph". Not-free means that the value of x cannot affect the value of ph, e.g., any occurrence of x in ph is effectively bound by a "for all" or something that expands to one (such as "there exists"). In particular, substitution for a variable not free in a wff does not affect its value (sbf 2107). An example of where this is used is stdpc5 1894. See nf2 1946 for an alternative definition which does not involve nested quantifiers on the same variable. Not-free is a commonly used constraint, so it is useful to have a notation for it. Surprisingly, there is no common formal notation for it, so here we devise one. Our definition lets us work with the not-free notion within the logic itself rather than as a metalogical side condition. To be precise, our definition really means "effectively not free," because it is slightly less restrictive than the usual textbook definition for not-free (which only considers syntactic freedom). For example, x is effectively not free in the bare expression x = x (see nfequid 1778), even though x would be considered free in the usual textbook definition, because the value of x in the expression x = x cannot affect the truth of the expression (and thus substitution will not change the result). This predicate only applies to wffs. See df-nfc 2593 for a not-free predicate for class variables. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
1.4.2  Rule scheme ax-gen (Generalization)
Axiom	ax-gen 1605	Rule of Generalization. The postulated inference rule of predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved x = x, we can conclude A. x x = x or even A. y x = x. Theorem allt 29842 shows the special case A. x T.. Theorem spi 1850 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (Contributed by NM, 3-Jan-1993.)
|- ph   =>    |- A. x ph
Theorem	gen2 1606	Generalization applied twice. (Contributed by NM, 30-Apr-1998.)
|- ph   =>    |- A. x A. y ph
Theorem	mpg 1607	Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)
|- ( A. x ph -> ps )   &    |- ph   =>    |- ps
Theorem	mpgbi 1608	Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
|- ( A. x ph <-> ps )   &    |- ph   =>    |- ps
Theorem	mpgbir 1609	Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
|- ( ph <-> A. x ps )   &    |- ps   =>    |- ph
Theorem	nfi 1610	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 1611	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 1612	No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ph   =>    |- F/ x ph
Theorem	nftru 1613	The true constant has no free variables. (This can also be proven in one step with nfv 1694, but this proof does not use ax-5 1691.) (Contributed by Mario Carneiro, 6-Oct-2016.)
|- F/ x T.
Theorem	nex 1614	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
|- -. ph   =>    |- -. E. x ph
Theorem	nfnth 1615	No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.)
|- -. ph   =>    |- F/ x ph
Theorem	nffal 1616	The false constant has no free variables (see nftru 1613). (Contributed by BJ, 6-May-2019.)
|- F/ x F.
Theorem	sptruw 1617	Version of sp 1845 when ph is true. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.)
|- ph   =>    |- ( A. x ph -> ph )
1.4.3  Axiom scheme ax-4 (Quantified Implication)
Axiom	ax-4 1618	Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1619 for labelling consistency. It should be used only by alim 1619. (Contributed by NM, 21-May-2008.) (New usage is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	alim 1619	Restatement of Axiom ax-4 1618, for labelling consistency. It should be the only theorem using ax-4 1618. (Contributed by NM, 10-Jan-1993.)
|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
Theorem	alimi 1620	Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	2alimi 1621	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	al2im 1622	Closed form of al2imi 1623. Version of ax-4 1618 for a nested implication. (Contributed by Alan Sare, 31-Dec-2011.)
|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )
Theorem	al2imi 1623	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 1624	Variant of al2imi 1623 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( A. x ph /\ A. x ps ) -> A. x ch )
Theorem	alimdh 1625	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1619. (Contributed by NM, 4-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	albi 1626	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 1627	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 1628	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 1629	Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1891 and 19.21h 1893. (Contributed by NM, 9-Jan-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	hbxfrbi 1630	A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2565 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ps )   &    |- ( ps -> A. x ps )   =>    |- ( ph -> A. x ph )
Theorem	nfbii 1631	Equality theorem for not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph <-> ps )   =>    |- ( F/ x ph <-> F/ x ps )
Theorem	nfxfr 1632	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 1633	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 1634	Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.)
|- ( A. x ph <-> -. E. x -. ph )
Theorem	exnal 1635	Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( E. x -. ph <-> -. A. x ph )
Theorem	2nalexn 1636	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 1637	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 1638	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	alimex 1639	A utility theorem. An interesting case is when the same formula is substituted for both ph and ps, since then both implications express a type of non-freeness. See also eximal 1602. (Contributed by BJ, 12-May-2019.)
|- ( ( ph -> A. x ps ) <-> ( E. x -. ps -> -. ph ) )
Theorem	aleximi 1640	A variant of al2imi 1623: instead of applying A. x quantifiers to the final implication, replace them with E. x. A shorter proof is possible using nfa1 1883, sps 1851 and eximd 1868, 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 1641	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 1642	Obsolete proof of exim 1641 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 1643	Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
|- ( ph -> ps )   =>    |- ( E. x ph -> E. x ps )
Theorem	2eximi 1644	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 1645	Inference associated with eximi 1643. (Contributed by BJ, 3-Feb-2018.)
|- E. x ph   &    |- ( ph -> ps )   =>    |- E. x ps
Theorem	aleximiOLD 1646	Obsolete proof of aleximi 1640 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	ala1 1647	Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.)
|- ( A. x ph -> A. x ( ps -> ph ) )
Theorem	exa1 1648	Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.)
|- ( E. x ph -> E. x ( ps -> ph ) )
Theorem	19.38 1649	Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 1890 and 19.23t 1895. (Revised by Wolf Lammen, 2-Jan-2018.)
|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
Theorem	alinexa 1650	A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
|- ( A. x ( ph -> -. ps ) <-> -. E. x ( ph /\ ps ) )
Theorem	alexn 1651	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 1652	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 1653	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 1654	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 1655	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 1656	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 1657	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 1658	Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
Theorem	alrimdh 1659	Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 1891 and 19.21h 1893. (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 1660	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 1661	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 1662	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 1663	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 1664	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 1665	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 1666	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 1667	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 1668	Theorem 19.26 1667 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 1669	Theorem 19.26 1667 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 1670	Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1671. (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 1671	Variation of 19.29 1670. (Contributed by NM, 18-Aug-1993.)
|- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) )
Theorem	19.29r2 1672	Variation of 19.29r 1671 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 1673	Variation of 19.29 1670 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 1674	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 1675	Obsolete proof of 19.35 1674 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 1676	Inference associated with 19.35 1674. (Contributed by NM, 21-Jun-1993.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> E. x ps )
Theorem	19.35ri 1677	Inference associated with 19.35 1674. (Contributed by NM, 12-Mar-1993.)
|- ( A. x ph -> E. x ps )   =>    |- E. x ( ph -> ps )
Theorem	19.25 1678	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 1679	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 1680	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 1681	Obsolete proof of 19.43 1680 as of 3-May-2099. Leave this in for the example on the mmrecent.html page and in conventions 25101. (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 1682	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 1683	The antecedent provides a condition implying the converse of 19.33 1682. (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 1684	Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with two 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	19.40b 1685	The antecedent provides a condition implying the converse of 19.40 1666. This is to 19.40 1666 what 19.33b 1683 is to 19.33 1682. (Contributed by BJ, 6-May-2019.)
|- ( ( A. x ph \/ A. x ps ) -> ( ( E. x ph /\ E. x ps ) <-> E. x ( ph /\ ps ) ) )
Theorem	albiim 1686	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 1687	Split a biconditional and distribute two 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 1688	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 1689	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 1690	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 1691*	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 2222 about the logical redundancy of ax-5 1691 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 1845, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-1993.)
|- ( ph -> A. x ph )
Theorem	ax5d 1692*	ax-5 1691 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 1693*	A rephrasing of ax-5 1691 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.)
|- ( E. x ph -> ph )
Theorem	nfv 1694*	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 1695*	nfv 1694 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1903. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- ( ph -> F/ x ps )
Theorem	alimdv 1696*	Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1619. (Contributed by NM, 3-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	eximdv 1697*	Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1641. (Contributed by NM, 27-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	2alimdv 1698*	Deduction form of Theorem 19.20 of [Margaris] p. 90 with two quantifiers, see alim 1619. (Contributed by NM, 27-Apr-2004.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x A. y ps -> A. x A. y ch ) )
Theorem	2eximdv 1699*	Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1641. (Contributed by NM, 3-Aug-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )
Theorem	albidv 1700*	Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )