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	hbal 1501	If x is not free in ph, it is not free in A. y ph. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( A. y ph -> A. x A. y ph )
Theorem	alcom 1502	Theorem 19.5 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
|- ( A. x A. y ph <-> A. y A. x ph )
Theorem	alrimdh 1503	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 1504	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 1505	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 1506	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 1507	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 1508	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 1509	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 1510	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 1511	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 1512	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 1513	Deduction form of bound-variable hypothesis builder hban 1571. (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 1514	Deduction form of bound-variable hypothesis builder hb3an 1574. (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 1515	Deduction form of bound-variable hypothesis builder hbal 1501. (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 1516	Extend wff definition to include the existential quantifier ("there exists").
wff E. x ph
Axiom	ax-ie1 1517	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 1518	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 1519	x is not free in E. x ph. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ph -> A. x E. x ph )
Theorem	nfe1 1520	x is not free in E. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x E. x ph
Theorem	19.23ht 1521	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 1522	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 1523	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 1525 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 1524	Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)
|- -. ph   =>    |- -. E. x ph
Theorem	dfexdc 1525	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 1526. (Contributed by Jim Kingdon, 15-Mar-2018.)
|- (DECID E. x ph -> ( E. x ph <-> -. A. x -. ph ) )
Theorem	exalim 1526	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 1525. (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 1373 for use by df-tru 1376. See the comments in that section. In this section, we continue with the first "real" use of it.
Theorem	weq 1527	Extend wff definition to include atomic formulas using the equality predicate. (Instead of introducing weq 1527 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 1373. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1527 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1373. 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 1528	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 1733). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105. Axioms ax-8 1528 through ax-16 1838 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 1838 and ax-17 1550 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 1838 and ax-17 1550 only. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( x = z -> y = z ) )
Axiom	ax-10 1529	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 1740 ("o" for "old") and was replaced with this shorter ax-10 1529 in May 2008. The old axiom is proved from this one as Theorem ax10o 1739. Conversely, this axiom is proved from ax-10o 1740 as Theorem ax10 1741. (Contributed by NM, 5-Aug-1993.)
|- ( A. x x = y -> A. y y = x )
Axiom	ax-11 1530	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 1911). 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 1851, ax11v2 1844 and ax-11o 1847. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Axiom	ax-i12 1531	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 1536 for compatibility with intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias ax12or 1532 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 1532	Alias for ax-i12 1531, 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 1533	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 1531 as can be seen at axi12 1538. Whether ax-bndl 1533 can be proved from the remaining axioms including ax-i12 1531 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 1534	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 1473. Conditional forms of the converse are given by ax12 1536, ax-16 1838, and ax-17 1550. 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 1799. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ph )
Theorem	sp 1535	Specialization. Another name for ax-4 1534. (Contributed by NM, 21-May-2008.)
|- ( A. x ph -> ph )
Theorem	ax12 1536	Rederive the original version of the axiom from ax-i12 1531. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
Theorem	hbequid 1537	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 1528 and ax-i12 1531 on top of (the FOL analogue of) modal logic KT. This shows that this can be proved without ax-i9 1554, even though Theorem equid 1725 cannot. A shorter proof using ax-i9 1554 is obtainable from equid 1725 and hbth 1487. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.)
|- ( x = x -> A. y x = x )
Theorem	axi12 1538	Proof that ax-i12 1531 follows from ax-bndl 1533. So that we can track which theorems rely on ax-bndl 1533, proofs should reference ax12or 1532 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 1539	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 1540	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 1541	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 1542	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.)
|- ( F/ x ph -> ( ph -> A. x ph ) )
Theorem	nfri 1543	Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- ( ph -> A. x ph )
Theorem	nfrd 1544	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 1545	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 1546	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 1547	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 1548	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 1549	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 1550*	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 1551*	ax-17 1550 with antecedent. (Contributed by NM, 1-Mar-2013.)
|- ( ph -> ( ps -> A. x ps ) )
Theorem	nfv 1552*	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 1553*	nfv 1552 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1609. (Contributed by Mario Carneiro, 6-Oct-2016.)
|- ( ph -> F/ x ps )
1.3.4  Introduce Axiom of Existence
Axiom	ax-i9 1554	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 1534 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 1720, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.)
|- E. x x = y
Theorem	ax-9 1555	Derive ax-9 1555 from ax-i9 1554, the modified version for intuitionistic logic. Although ax-9 1555 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1554. (Contributed by NM, 3-Feb-2015.)
|- -. A. x -. x = y
Theorem	equidqe 1556	equid 1725 with some quantification and negation without using ax-4 1534 or ax-17 1550. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.)
|- -. A. y -. x = x
Theorem	ax4sp1 1557	A special case of ax-4 1534 without using ax-4 1534 or ax-17 1550. (Contributed by NM, 13-Jan-2011.)
|- ( A. y -. x = x -> -. x = x )
1.3.5  Additional intuitionistic axioms
Axiom	ax-ial 1558	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 1559	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 1560	Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.)
|- A. x ph   =>    |- ph
Theorem	sps 1561	Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	spsd 1562	Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
Theorem	nfbidf 1563	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 1564	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 1565	x is not free in A. x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x A. x ph
Theorem	axc4i 1566	Inference version of 19.21 1607. (Contributed by NM, 3-Jan-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	a5i 1567	Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.)
|- ( A. x ph -> ps )   =>    |- ( A. x ph -> A. x ps )
Theorem	nfnf1 1568	x is not free in F/ x ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/ x ph
Theorem	hbim 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 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 1570	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 1571	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 1572	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 1573	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 1574	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 1575	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 1576	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 1577	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 1578	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 1579	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 1580	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 1581	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 1607 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 1582	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ps )   =>    |- ( ph -> ps )
Theorem	19.21bbi 1583	Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> A. x A. y ps )   =>    |- ( ph -> ps )
Theorem	19.27h 1584	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 1585	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 1586	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 1587	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 1588	A closed form of nfan 1589. (Contributed by Mario Carneiro, 3-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ps )   =>    |- F/ x ( ph /\ ps )
Theorem	nfan 1589	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 1590	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 1591	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 1592	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 1593	Deduction form of bound-variable hypothesis builder nf3an 1590. (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 1594	A closed form of hbim 1569. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ( ph -> ps ) -> A. x ( ph -> ps ) )
Theorem	nfim1 1595	A closed form of nfim 1596. (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 1596	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 1597	Deduction form of bound-variable hypothesis builder hbim 1569. (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 1598	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 1599	Deduction form of bound-variable hypothesis builder hbbi 1572. (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 1600	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 1534. (Revised by GG, 25-Aug-2024.)
|- F/ x ph   =>    |- F/ x A. y ph