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	alrimdh 1501	Deduction from Theorem 19.21 of [Margaris] p. 90. (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	albidh 1502	Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. x ch ) )
Theorem	19.26 1503	Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )
Theorem	19.26-2 1504	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 1505	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.33 1506	Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) )
Theorem	alrot3 1507	Theorem *11.21 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y A. z ph <-> A. y A. z A. x ph )
Theorem	alrot4 1508	Rotate 4 universal quantifiers twice. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 28-Jun-2014.)
|- ( A. x A. y A. z A. w ph <-> A. z A. w A. x A. y ph )
Theorem	albiim 1509	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 1510	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	hband 1511	Deduction form of bound-variable hypothesis builder hban 1569. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps /\ ch ) -> A. x ( ps /\ ch ) ) )
Theorem	hb3and 1512	Deduction form of bound-variable hypothesis builder hb3an 1572. (Contributed by NM, 17-Feb-2013.)
|- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   &    |- ( ph -> ( th -> A. x th ) )   =>    |- ( ph -> ( ( ps /\ ch /\ th ) -> A. x ( ps /\ ch /\ th ) ) )
Theorem	hbald 1513	Deduction form of bound-variable hypothesis builder hbal 1499. (Contributed by NM, 2-Jan-2002.)
|- ( ph -> A. y ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( A. y ps -> A. x A. y ps ) )
Syntax	wex 1514	Extend wff definition to include the existential quantifier ("there exists").
wff E. x ph
Axiom	ax-ie1 1515	x is bound in E. x ph. One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( E. x ph -> A. x E. x ph )
Axiom	ax-ie2 1516	Define existential quantification. E. x ph means "there exists at least one set x such that ph is true". One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	hbe1 1517	x is not free in E. x ph. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ph -> A. x E. x ph )
Theorem	nfe1 1518	x is not free in E. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x E. x ph
Theorem	19.23ht 1519	Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 1-Feb-2015.)
|- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) )
Theorem	19.23h 1520	Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 1-Feb-2015.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	alnex 1521	Theorem 19.7 of [Margaris] p. 89. To read this intuitionistically, think of it as "if ph can be refuted for all x, then it is not possible to find an x for which ph holds" (and likewise for the converse). Comparing this with dfexdc 1523 illustrates that statements which look similar (to someone used to classical logic) can be different intuitionistically due to different placement of negations. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 1-Feb-2015.) (Revised by Mario Carneiro, 12-May-2015.)
|- ( A. x -. ph <-> -. E. x ph )
Theorem	nex 1522	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
|- -. ph   =>    |- -. E. x ph
Theorem	dfexdc 1523	Defining E. x ph given decidability. It is common in classical logic to define E. x ph as -. A. x -. ph but in intuitionistic logic without a decidability condition, that is only an implication not an equivalence, as seen at exalim 1524. (Contributed by Jim Kingdon, 15-Mar-2018.)
|- (DECID E. x ph -> ( E. x ph <-> -. A. x -. ph ) )
Theorem	exalim 1524	One direction of a classical definition of existential quantification. One direction of Definition of [Margaris] p. 49. For a decidable proposition, this is an equivalence, as seen as dfexdc 1523. (Contributed by Jim Kingdon, 29-Jul-2018.)
|- ( E. x ph -> -. A. x -. ph )
1.3.2  Equality predicate (continued) The equality predicate was introduced above in wceq 1372 for use by df-tru 1375. See the comments in that section. In this section, we continue with the first "real" use of it.
Theorem	weq 1525	Extend wff definition to include atomic formulas using the equality predicate. (Instead of introducing weq 1525 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 1372. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1525 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1372. 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
Axiom	ax-8 1526	Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. This is similar to, but not quite, a transitive law for equality (proved later as equtr 1731). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. Axioms ax-8 1526 through ax-16 1836 are the axioms having to do with equality, substitution, and logical properties of our binary predicate e. (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1836 and ax-17 1548 are still valid even when x, y, and z are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 1836 and ax-17 1548 only. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( x = z -> y = z ) )
Axiom	ax-10 1527	Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). The original version of this axiom was ax-10o 1738 ("o" for "old") and was replaced with this shorter ax-10 1527 in May 2008. The old axiom is proved from this one as Theorem ax10o 1737. Conversely, this axiom is proved from ax-10o 1738 as Theorem ax10 1739. (Contributed by NM, 5-Aug-1993.)
|- ( A. x x = y -> A. y y = x )
Axiom	ax-11 1528	Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent A. x ( x = y -> ph ) is a way of expressing " y substituted for x in wff ph " (cf. sb6 1909). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. Variants of this axiom which are equivalent in classical logic but which have not been shown to be equivalent for intuitionistic logic are ax11v 1849, ax11v2 1842 and ax-11o 1845. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Axiom	ax-i12 1529	Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. This axiom has been modified from the original ax12 1534 for compatibility with intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias ax12or 1530 instead, for labeling consistency. (New usage is discouraged.)
|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
Theorem	ax12or 1530	Alias for ax-i12 1529, to be used in place of it for labeling consistency. (Contributed by NM, 3-Feb-2015.)
|- ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) )
Axiom	ax-bndl 1531	Axiom of bundling. The general idea of this axiom is that two variables are either distinct or non-distinct. That idea could be expressed as A. z z = x \/ -. A. z z = x. However, we instead choose an axiom which has many of the same consequences, but which is different with respect to a universe which contains only one object. A. z z = x holds if z and x are the same variable, likewise for z and y, and A. x A. z ( x = y -> A. z x = y ) holds if z is distinct from the others (and the universe has at least two objects). As with other statements of the form "x is decidable (either true or false)", this does not entail the full Law of the Excluded Middle (which is the proposition that all statements are decidable), but instead merely the assertion that particular kinds of statements are decidable (or in this case, an assertion similar to decidability). This axiom implies ax-i12 1529 as can be seen at axi12 1536. Whether ax-bndl 1531 can be proved from the remaining axioms including ax-i12 1529 is not known. The reason we call this "bundling" is that a statement without a distinct variable constraint "bundles" together two statements, one in which the two variables are the same and one in which they are different. (Contributed by Mario Carneiro and Jim Kingdon, 14-Mar-2018.)
|- ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) )
Axiom	ax-4 1532	Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all x, it is true for any specific x (that would typically occur as a free variable in the wff substituted for ph). (A free variable is one that does not occur in the scope of a quantifier: x and y are both free in x = y, but only x is free in A. y x = y.) Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77). Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1471. Conditional forms of the converse are given by ax12 1534, ax-16 1836, and ax-17 1548. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1797. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ph )
Theorem	sp 1533	Specialization. Another name for ax-4 1532. (Contributed by NM, 21-May-2008.)
|- ( A. x ph -> ph )
Theorem	ax12 1534	Rederive the original version of the axiom from ax-i12 1529. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
Theorem	hbequid 1535	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-8 1526 and ax-i12 1529 on top of (the FOL analogue of) modal logic KT. This shows that this can be proved without ax-i9 1552, even though Theorem equid 1723 cannot. A shorter proof using ax-i9 1552 is obtainable from equid 1723 and hbth 1485. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.)
|- ( x = x -> A. y x = x )
Theorem	axi12 1536	Proof that ax-i12 1529 follows from ax-bndl 1531. So that we can track which theorems rely on ax-bndl 1531, proofs should reference ax12or 1530 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 1537	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 1538	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 1539	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 1540	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
|- ( F/ x ph -> ( ph -> A. x ph ) )
Theorem	nfri 1541	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- ( ph -> A. x ph )
Theorem	nfrd 1542	Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/ x ps )   =>    |- ( ph -> ( ps -> A. x ps ) )
Theorem	alimd 1543	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	alrimi 1544	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	nfd 1545	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfdh 1546	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	nfrimi 1547	Moving an antecedent outside F/. (Contributed by Jim Kingdon, 23-Mar-2018.)
|- F/ x ph   &    |- F/ x ( ph -> ps )   =>    |- ( ph -> F/ x ps )
1.3.3  Axiom ax-17 - first use of the $d distinct variable statement
Axiom	ax-17 1548*	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. x ph )
Theorem	a17d 1549*	ax-17 1548 with antecedent. (Contributed by NM, 1-Mar-2013.)
|- ( ph -> ( ps -> A. x ps ) )
Theorem	nfv 1550*	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 1551*	nfv 1550 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1607. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- ( ph -> F/ x ps )
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1552	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 1532 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 1718, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- E. x x = y
Theorem	ax-9 1553	Derive ax-9 1553 from ax-i9 1552, the modified version for intuitionistic logic. Although ax-9 1553 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1552. (Contributed by NM, 3-Feb-2015.)
|- -. A. x -. x = y
Theorem	equidqe 1554	equid 1723 with some quantification and negation without using ax-4 1532 or ax-17 1548. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
|- -. A. y -. x = x
Theorem	ax4sp1 1555	A special case of ax-4 1532 without using ax-4 1532 or ax-17 1548. (Contributed by NM, 13-Jan-2011.)
|- ( A. y -. x = x -> -. x = x )
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1556	x is not free in A. x ph. One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( A. x ph -> A. x A. x ph )
Axiom	ax-i5r 1557	Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> ps ) )
1.3.6  Predicate calculus including ax-4, without distinct variables
Theorem	spi 1558	Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.)
|- A. x ph   =>    |- ph
Theorem	sps 1559	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	spsd 1560	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
Theorem	nfbidf 1561	An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( F/ x ps <-> F/ x ch ) )
Theorem	hba1 1562	x is not free in A. x ph. 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. x ph -> A. x A. x ph )
Theorem	nfa1 1563	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x A. x ph
Theorem	axc4i 1564	Inference version of 19.21 1605. (Contributed by NM, 3-Jan-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	a5i 1565	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	nfnf1 1566	x is not free in F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/ x ph
Theorem	hbim 1567	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. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	hbor 1568	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. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph \/ ps ) -> A. x ( ph \/ ps ) )
Theorem	hban 1569	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. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph /\ ps ) -> A. x ( ph /\ ps ) )
Theorem	hbbi 1570	If x is not free in ph and ps, it is not free in ( ph <-> ps ). (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   =>    |- ( ( ph <-> ps ) -> A. x ( ph <-> ps ) )
Theorem	hb3or 1571	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. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph \/ ps \/ ch ) -> A. x ( ph \/ ps \/ ch ) )
Theorem	hb3an 1572	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. x ph )   &    |- ( ps -> A. x ps )   &    |- ( ch -> A. x ch )   =>    |- ( ( ph /\ ps /\ ch ) -> A. x ( ph /\ ps /\ ch ) )
Theorem	hba2 1573	Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- ( A. y A. x ph -> A. x A. y A. x ph )
Theorem	hbia1 1574	Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.)
|- ( ( A. x ph -> A. x ps ) -> A. x ( A. x ph -> A. x ps ) )
Theorem	19.3h 1575	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. x ph )   =>    |- ( A. x ph <-> ph )
Theorem	19.3 1576	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/ x ph   =>    |- ( A. x ph <-> ph )
Theorem	19.16 1577	Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ph   =>    |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) )
Theorem	19.17 1578	Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- F/ x ps   =>    |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) )
Theorem	19.21h 1579	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 1605 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	19.21bi 1580	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ps )   =>    |- ( ph -> ps )
Theorem	19.21bbi 1581	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> A. x A. y ps )   =>    |- ( ph -> ps )
Theorem	19.27h 1582	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ps -> A. x ps )   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.27 1583	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ps   =>    |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28h 1584	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	19.28 1585	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- F/ x ph   =>    |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	nfan1 1586	A closed form of nfan 1587. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1587	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/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph /\ ps )
Theorem	nf3an 1588	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/ x ph   &    |- F/ x ps   &    |- F/ x ch   =>    |- F/ x ( ph /\ ps /\ ch )
Theorem	nford 1589	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/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps \/ ch ) )
Theorem	nfand 1590	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/ x ps )   &    |- ( ph -> F/ x ch )   =>    |- ( ph -> F/ x ( ps /\ ch ) )
Theorem	nf3and 1591	Deduction form of bound-variable hypothesis builder nf3an 1588. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.)
|- ( ph -> F/ x ps )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> F/ x th )   =>    |- ( ph -> F/ x ( ps /\ ch /\ th ) )
Theorem	hbim1 1592	A closed form of hbim 1567. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1593	A closed form of nfim 1594. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph -> ps )
Theorem	nfim 1594	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/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph -> ps )
Theorem	hbimd 1595	Deduction form of bound-variable hypothesis builder hbim 1567. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps -> ch ) -> A. x ( ps -> ch ) ) )
Theorem	nfor 1596	If x is not free in ph and ps, it is not free in ( ph \/ ps ). (Contributed by Jim Kingdon, 11-Mar-2018.)
|- F/ x ph   &    |- F/ x ps   =>    |- F/ x ( ph \/ ps )
Theorem	hbbid 1597	Deduction form of bound-variable hypothesis builder hbbi 1570. (Contributed by NM, 1-Jan-2002.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   &    |- ( ph -> ( ch -> A. x ch ) )   =>    |- ( ph -> ( ( ps <-> ch ) -> A. x ( ps <-> ch ) ) )
Theorem	nfal 1598	If x is not free in ph, it is not free in A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1532. (Revised by GG, 25-Aug-2024.)
|- F/ x ph   =>    |- F/ x A. y ph
Theorem	nfnf 1599	If x is not free in ph, it is not free in F/ y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
|- F/ x ph   =>    |- F/ x F/ y ph
Theorem	nfalt 1600	Closed form of nfal 1598. (Contributed by Jim Kingdon, 11-May-2018.)
|- ( A. y F/ x ph -> F/ x A. y ph )