Metamath Proof Explorer - mmtheorems7

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 601-700 - Page 7 of 58

Type	Label	Description
Statement
Theorem	3mix2 601	Introduction in triple disjunction.
⊢ (φ → (ψ ∨ φ ∨ χ))
Theorem	3mix3 602	Introduction in triple disjunction.
⊢ (φ → (ψ ∨ χ ∨ φ))
Theorem	3pm3.2i 603	Infer conjunction of premises.
⊢ φ    &   ⊢ ψ    &   ⊢ χ    ⇒   ⊢ (φ ∧ ψ ∧ χ)
Theorem	3jca 604	Join consequents with conjunction.
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ ∧ χ ∧ θ))
Theorem	im3an 605	Join antecedents and consequents with conjunction.
⊢ (φ → ψ)    &   ⊢ (χ → θ)    &   ⊢ (τ → η)    ⇒   ⊢ ((φ ∧ χ ∧ τ) → (ψ ∧ θ ∧ η))
Theorem	bi3an 606	Join 3 biconditionals with conjunction.
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    &   ⊢ (τ ↔ η)    ⇒   ⊢ ((φ ∧ χ ∧ τ) ↔ (ψ ∧ θ ∧ η))
Theorem	bi3or 607	Join antecedents and consequents with disjunction.
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    &   ⊢ (τ ↔ η)    ⇒   ⊢ ((φ ∨ χ ∨ τ) ↔ (ψ ∨ θ ∨ η))
Theorem	3imp 608	Importation inference.
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impa 609	Importation from double to triple conjunction.
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impb 610	Importation from double to triple conjunction.
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3exp 611	Exportation inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	3expa 612	Exportation from triple to double conjunction.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → θ)
Theorem	3expb 613	Exportation from triple to double conjunction.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)
Theorem	3com12 614	Commutation in antecedent. Swap 1st and 3rd.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ φ ∧ χ) → θ)
Theorem	3com13 615	Commutation in antecedent. Swap 1st and 3rd.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((χ ∧ ψ ∧ φ) → θ)
Theorem	3com23 616	Commutation in antecedent. Swap 2nd and 3rd.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ χ ∧ ψ) → θ)
Theorem	3coml 617	Commutation in antecedent. Rotate left.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ χ ∧ φ) → θ)
Theorem	3comr 618	Commutation in antecedent. Rotate right.
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((χ ∧ φ ∧ ψ) → θ)
Theorem	syl3an1 619	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ → φ)    ⇒   ⊢ ((τ ∧ ψ ∧ χ) → θ)
Theorem	syl3an2 620	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ → ψ)    ⇒   ⊢ ((φ ∧ τ ∧ χ) → θ)
Theorem	syl3an3 621	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ → χ)    ⇒   ⊢ ((φ ∧ ψ ∧ τ) → θ)
Theorem	syl3an1b 622	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ ↔ φ)    ⇒   ⊢ ((τ ∧ ψ ∧ χ) → θ)
Theorem	syl3an2b 623	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ ↔ ψ)    ⇒   ⊢ ((φ ∧ τ ∧ χ) → θ)
Theorem	syl3an3b 624	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ ↔ χ)    ⇒   ⊢ ((φ ∧ ψ ∧ τ) → θ)
Theorem	syl3an1br 625	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (φ ↔ τ)    ⇒   ⊢ ((τ ∧ ψ ∧ χ) → θ)
Theorem	syl3an2br 626	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (ψ ↔ τ)    ⇒   ⊢ ((φ ∧ τ ∧ χ) → θ)
Theorem	syl3an3br 627	A syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (χ ↔ τ)    ⇒   ⊢ ((φ ∧ ψ ∧ τ) → θ)
Theorem	syl3an 628	A triple syllogism inference.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ → φ)    &   ⊢ (η → ψ)    &   ⊢ (ζ → χ)    ⇒   ⊢ ((τ ∧ η ∧ ζ) → θ)
Theorem	syl3anc 629	A syllogism inference combined with contraction.
⊢ ((φ ∧ ψ ∧ χ) → θ)    &   ⊢ (τ → φ)    &   ⊢ (τ → ψ)    &   ⊢ (τ → χ)    ⇒   ⊢ (τ → θ)
Theorem	3impdi 630	Importation inference (undistribute conjunction).
⊢ (((φ ∧ ψ) ∧ (φ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impdir 631	Importation inference (undistribute conjunction).
⊢ (((φ ∧ ψ) ∧ (χ ∧ ψ)) → θ)    ⇒   ⊢ ((φ ∧ χ ∧ ψ) → θ)
Theorem	3jao 632	Disjunction of 3 antecedents.
⊢ (((φ → ψ) ∧ (χ → ψ) ∧ (θ → ψ)) → ((φ ∨ χ ∨ θ) → ψ))
Theorem	3jaoi 633	Disjunction of 3 antecedents (inference).
⊢ (φ → ψ)    &   ⊢ (χ → ψ)    &   ⊢ (θ → ψ)    ⇒   ⊢ ((φ ∨ χ ∨ θ) → ψ)
Theorem	syl3an9b 634	Nested syllogism inference conjoining 3 dissimilar antecedents.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (θ → (χ ↔ τ))    &   ⊢ (η → (τ ↔ ζ))    ⇒   ⊢ ((φ ∧ θ ∧ η) → (ψ ↔ ζ))
Theorem	bi3ord 635	Deduction joining 3 equivalences to form equivalence of disjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    &   ⊢ (φ → (η ↔ ζ))    ⇒   ⊢ (φ → ((ψ ∨ θ ∨ η) ↔ (χ ∨ τ ∨ ζ)))
Theorem	bi3and 636	Deduction joining 3 equivalences to form equivalence of conjunctions.
⊢ (φ → (ψ ↔ χ))    &   ⊢ (φ → (θ ↔ τ))    &   ⊢ (φ → (η ↔ ζ))    ⇒   ⊢ (φ → ((ψ ∧ θ ∧ η) ↔ (χ ∧ τ ∧ ζ)))
Theorem	im3ord 637	Deduction joining 3 implications to form implication of disjunctions.
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (θ → τ))    &   ⊢ (φ → (η → ζ))    ⇒   ⊢ (φ → ((ψ ∨ θ ∨ η) → (χ ∨ τ ∨ ζ)))
Theorem	an6 638	Rearrangement of 6 conjuncts.
⊢ (((φ ∧ ψ ∧ χ) ∧ (θ ∧ τ ∧ η)) ↔ ((φ ∧ θ) ∧ (ψ ∧ τ) ∧ (χ ∧ η)))
Theorem	mp3an1 639	An inference based on modus ponens.
⊢ φ    &   ⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ χ) → θ)
Theorem	mp3an2 640	An inference based on modus ponens.
⊢ ψ    &   ⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ χ) → θ)
Theorem	mp3an3 641	An inference based on modus ponens.
⊢ χ    &   ⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ) → θ)
Theorem	mp3an 642	An inference based on modus ponens.
⊢ φ    &   ⊢ ψ    &   ⊢ χ    &   ⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ θ
Theorem	ecased 643	Deduction for elimination by cases.
⊢ (φ → (ψ ∨ χ ∨ θ))    &   ⊢ (φ → ¬ χ)    &   ⊢ (φ → ¬ θ)    ⇒   ⊢ (φ → ψ)
Theorem	meredith 644	Carew Meredith's sole axiom for propositional calculus. This amazing formula is thought to be the shortest possible single axiom for propositional calculus using negation, implication, and inference rule ax-mp 6. Here we prove Meredith's axiom from ax-1 3, ax-2 4, and ax-3 5. Then from it we derive the Lukasiewicz axioms luk-1 658, luk-2 659, and luk-3 660. Using these we finally re-derive our axioms as ax1 669, ax2 670, and ax3 671, thus proving the equivalence of all three systems. C. A. Meredith, "Single Axioms for the Systems (C,N), (C,O) and (A,N) of the Two-Valued Propositional Calculus", The Journal of Computing Systems vol. 3 (1953), pp. 155-164. Meredith claimed to be close to a proof that this axiom is the shortest possible, but the proof was apparently never completed. An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues."
⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))
Theorem	merlem1 645	Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
⊢ (((χ → (¬ φ → ψ)) → τ) → (φ → τ))
Theorem	merlem2 646	Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (((φ → φ) → χ) → (θ → χ))
Theorem	merlem3 647	Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (((ψ → χ) → φ) → (χ → φ))
Theorem	merlem4 648	Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (τ → ((τ → φ) → (θ → φ)))
Theorem	merlem5 649	Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ ((φ → ψ) → (¬ ¬ φ → ψ))
Theorem	merlem6 650	Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (χ → (((ψ → χ) → φ) → (θ → φ)))
Theorem	merlem7 651	Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (φ → (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ)))
Theorem	merlem8 652	Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (((ψ → χ) → θ) → (((χ → τ) → (¬ θ → ¬ ψ)) → θ))
Theorem	merlem9 653	Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (((φ → ψ) → (χ → (θ → (ψ → τ)))) → (η → (χ → (θ → (ψ → τ)))))
Theorem	merlem10 654	Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ ((φ → (φ → ψ)) → (θ → (φ → ψ)))
Theorem	merlem11 655	Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ ((φ → (φ → ψ)) → (φ → ψ))
Theorem	merlem12 656	Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ (((θ → (¬ ¬ χ → χ)) → φ) → φ)
Theorem	merlem13 657	Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
⊢ ((φ → ψ) → (((θ → (¬ ¬ χ → χ)) → ¬ ¬ φ) → ψ))
Theorem	luk-1 658	1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))
Theorem	luk-2 659	2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
⊢ ((¬ φ → φ) → φ)
Theorem	luk-3 660	3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
⊢ (φ → (¬ φ → ψ))
Theorem	luklem1 661	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ (φ → ψ)    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	luklem2 662	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ ((φ → ¬ ψ) → (((φ → χ) → θ) → (ψ → θ)))
Theorem	luklem3 663	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ (φ → (((¬ φ → ψ) → χ) → (θ → χ)))
Theorem	luklem4 664	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ ((((¬ φ → φ) → φ) → ψ) → ψ)
Theorem	luklem5 665	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ (φ → (ψ → φ))
Theorem	luklem6 666	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ ((φ → (φ → ψ)) → (φ → ψ))
Theorem	luklem7 667	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ)))
Theorem	luklem8 668	Lemma for rederiving standard propositional axioms from Lukasiewicz'.
⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ)))
Theorem	ax1 669	Standard propositional axiom derived from Lukasiewicz axioms.
⊢ (φ → (ψ → φ))
Theorem	ax2 670	Standard propositional axiom derived from Lukasiewicz axioms.
⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
Theorem	ax3 671	Standard propositional axiom derived from Lukasiewicz axioms.
⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
Syntax	wal 672	Extend wff definition to include the universal quantifier ('for all'). ∀xφ is read "φ (phi) is true for all x." Typically, in its final application φ would be replaced with a wff containing a (free) occurrence of the variable x, for example x = y. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of x. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
wff ∀xφ
Axiom	ax-4 673	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 φ). (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 y is free in ∀xx = y.) This is one of the 4 axioms of what we call "pure" predicate calculus. Unlike the more typical textbook Axiom of Specialization, we cannot choose a variable different from x for the special case. That is dealt with later when substitution is introduced - see stdpc4 869. 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 677. Conditional forms of the converse are given by ax-12 802, ax-15 806, ax-16 922, and ax-17 925.
⊢ (∀xφ → φ)
Axiom	ax-5 674	Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying ψ. Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding φ to "protect" the axiom from a φ containing a free x. One of the 4 axioms of pure predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108.
⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
Axiom	ax-6 675	Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). Another equivalent variant ax6 711 appears as Axiom C5-2 of [Monk2] p. 113.
⊢ (¬ ∀x ¬ ∀xφ → φ)
Axiom	ax-7 676	Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. One of the 4 axioms of pure predicate calculus. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109.
⊢ (∀x∀yφ → ∀y∀xφ)
Axiom	ax-gen 677	Rule of Generalization. The postulated inference rule of pure 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 ∀xx = x or even ∀yx = x. Theorem a4i 680 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.
⊢ φ    ⇒   ⊢ ∀xφ
Syntax	wex 678	Extend wff definition to include the existential quantifier ("there exists").
wff ∃xφ
Definition	df-ex 679	Define existential quantification. ∃xφ means "there exists at least one set x such that φ is true." Definition of [Margaris] p. 49.
⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
Theorem	a4i 680	Inference rule reversing generalization.
⊢ ∀xφ    ⇒   ⊢ φ
Theorem	gen2 681	Generalization applied twice.
⊢ φ    ⇒   ⊢ ∀x∀yφ
Theorem	a4s 682	Generalization of antecedent.
⊢ (φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
Theorem	a4sd 683	Deduction generalizing antecedent.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀xψ → χ))
Theorem	mpg 684	Modus ponens combined with generalization.
⊢ (∀xφ → ψ)    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	mpgbi 685	Modus ponens on biconditional combined with generalization.
⊢ (∀xφ ↔ ψ)    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	mpgbir 686	Modus ponens on biconditional combined with generalization.
⊢ (φ ↔ ∀xψ)    &   ⊢ ψ    ⇒   ⊢ φ
Theorem	a5i 687	Inference from ax-5 674.
⊢ (∀xφ → ψ)    ⇒   ⊢ (∀xφ → ∀xψ)
Theorem	a6e 688	Abbreviated version of ax-6 675.
⊢ (∃x∀xφ → φ)
Theorem	a7s 689	Swap quantifiers in an antecedent.
⊢ (∀x∀yφ → ψ)    ⇒   ⊢ (∀y∀xφ → ψ)
Theorem	19.20 690	Theorem 19.20 of [Margaris] p. 90.
⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))
Theorem	19.20i 691	Inference quantifying both antecedent and consequent.
⊢ (φ → ψ)    ⇒   ⊢ (∀xφ → ∀xψ)
Theorem	19.20ii 692	Inference quantifying antecedent, nested antecedent, and consequent.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (∀xφ → (∀xψ → ∀xχ))
Theorem	19.20d 693	Deduction from Theorem 19.20 of [Margaris] p. 90.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀xψ → ∀xχ))
Theorem	19.15 694	Theorem 19.15 of [Margaris] p. 90.
⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ))
Theorem	bial 695	Inference adding universal quantifier to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀xφ ↔ ∀xψ)
Theorem	bi2al 696	Inference adding 2 universal quantifiers to both sides of an equivalence.
⊢ (φ ↔ ψ)    ⇒   ⊢ (∀x∀yφ ↔ ∀x∀yψ)
Theorem	hbth 697	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 ⊢ (φ → ∀xφ) from smaller formulas of this form. These are useful for constructing hypotheses that state "x is (effectively) not free in φ".
⊢ φ    ⇒   ⊢ (φ → ∀xφ)
Theorem	hba1 698	x is not free in ∀xφ. Appendix example in [Megill] p. 450 (p. 19 of the preprint).
⊢ (∀xφ → ∀x∀xφ)
Theorem	hbne 699	If x is not free in φ, it is not free in ¬ φ.
⊢ (φ → ∀xφ)    ⇒   ⊢ (¬ φ → ∀x ¬ φ)
Theorem	hbal 700	If x is not free in φ, it is not free in ∀yφ.
⊢ (φ → ∀xφ)    ⇒   ⊢ (∀yφ → ∀x∀yφ)