P. 9 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psubsplitelof-P6 801*	Apply Proper Substitution to Split "Element Of" Predicate. '𝑎' and '𝑏' are distinct form all other variables.
⊢ ([𝑤 / 𝑥] 𝑡 ∈ 𝑢 ↔ ∃𝑎∃𝑏(([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
7.6.5.2  Proper Substitution Applied to Atomic Terms.
Theorem	psubvar1-P6 802*	Proper Substitution Applied to Atomic Term (same variable). '𝑎' is distinct from all other variables.
⊢ ([𝑡 / 𝑥] 𝑎 = 𝑥 ↔ 𝑎 = 𝑡)
Theorem	psubvar2-P6 803*	Proper Substitution Applied to Atomic Term (different variable). '𝑎' is distinct from all other variables.
⊢ ([𝑡 / 𝑥] 𝑎 = 𝑦 ↔ 𝑎 = 𝑦)
Theorem	psubzero-P6 804*	Proper Substitution Applied to Atomic Term (constant). '𝑎' is distinct from all other variables.
⊢ ([𝑡 / 𝑥] 𝑎 = 0 ↔ 𝑎 = 0)
7.6.5.3  Proper Substitution Applied to Terms with Functions.
Theorem	psubsuccv-P6-L1 805*	Lemma for psubsuccv-P6 806. [Auxiliary lemma - not displayed.]
Theorem	psubsuccv-P6 806*	Proper Substitution Over Successor Function (variable restriction). '𝑎' and '𝑏' are distinct from all other variables and '𝑥' cannot occur in '𝑤'.
⊢ ([𝑤 / 𝑥] 𝑎 = 𝑡 ↔ 𝑎 = 𝑢)    ⇒   ⊢ ([𝑤 / 𝑥] 𝑏 = s‘𝑡 ↔ 𝑏 = s‘𝑢)
Theorem	psubaddv-P6-L1 807*	Lemma for psubaddv-P6 808. [Auxiliary lemma - not displayed.]
Theorem	psubaddv-P6 808*	Proper Substitution Over Addition (variable restriction). '𝑎', '𝑏', and '𝑐' are distinct from all other variables and '𝑥' cannot occur in '𝑤'.
⊢ ([𝑤 / 𝑥] 𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁)    &   ⊢ ([𝑤 / 𝑥] 𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂)    ⇒   ⊢ ([𝑤 / 𝑥] 𝑐 = (𝑡₁ + 𝑡₂) ↔ 𝑐 = (𝑢₁ + 𝑢₂))
Theorem	psubmultv-P6-L1 809*	Lemma for psubmultv-P6 810. [Auxiliary lemma - not displayed.]
Theorem	psubmultv-P6 810*	Proper Substitution Over Multiplication (variable restriction). '𝑎', '𝑏', and '𝑐' are distinct from all other variables and '𝑥' cannot occur in '𝑤'.
⊢ ([𝑤 / 𝑥] 𝑎 = 𝑡₁ ↔ 𝑎 = 𝑢₁)    &   ⊢ ([𝑤 / 𝑥] 𝑏 = 𝑡₂ ↔ 𝑏 = 𝑢₂)    ⇒   ⊢ ([𝑤 / 𝑥] 𝑐 = (𝑡₁ ⋅ 𝑡₂) ↔ 𝑐 = (𝑢₁ ⋅ 𝑢₂))
7.7  Deductive Forms.
7.7.1  Some Lemmas.
Theorem	nfrgencl-L6 811	Closed Form of nfrgen-P6 733.
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	gennfrcl-L6 812	Closed Form of gennfr-P6 734.
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
Theorem	nfrexgencl-L6 813	Closed Form of nfrexgen-P6 735.
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 → 𝜑))
Theorem	exgennfrcl-L6 814	Closed Form of exgennfr-P6 736.
⊢ (∀𝑥(∃𝑥𝜑 → 𝜑) → Ⅎ𝑥𝜑)
7.7.2  Effective Non-Freeness.
Theorem	nfrimd-P6 815	ENF Over Implication (deductive form).
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 → 𝜓))
Theorem	nfrandd-P6 816	ENF Over Conjunction (deductive form).
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ∧ 𝜓))
Theorem	nfrord-P6 817	ENF Over Disjunction (deductive form).
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ∨ 𝜓))
Theorem	nfrbid-P6 818	ENF Over Biconditional (deductive form).
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ↔ 𝜓))
Theorem	nfrall2d-P6 819*	ENF Over Universal Quantifier (different variable - deductive form).
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∀𝑦𝜑)
Theorem	nfrex2d-P6 820*	ENF Over Existential Quantifier (different variable - deductive form).
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∃𝑦𝜑)
Theorem	nfrnfr-P6 821	ENF Over ENF Predicate. Interpreted semantically, this says that the effective non-freeness predicate does not depend on the value assigned to the indicated variable, '𝑥'. This means effective non-freeness is a property of a WFF that will either be true for every '𝑥' assignment or false for every '𝑥' assignment. We expect this since ENF is a property that we should be able to determine grammatically.
⊢ Ⅎ𝑥Ⅎ𝑥𝜑
7.7.3  Universal Quantifier Introduction.
Theorem	ndalli-P6 822*	Natural Deduction Form of Universal Quantifier Introduction.
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → [𝑦 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
7.7.4  Exestential Quantifier Elimination.
Theorem	qremexd-P6 823	Existential Quantifier Removal Theorem (deductive form).
⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 ↔ 𝜑))
Theorem	exiad-P6 824	Introduction of Existential Quantifier as Antecedent (deductive form).
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	ndexe-P6 825*	Natural Deduction Form of Existential Quantifier Elimination.
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → Ⅎ𝑦𝜓)    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
PART 8  Chapter 7: Predicate Calculus (Natural Deduction)
8.1  Natural Deduction for Predicate Calculus.
8.1.1  Axiomatic Rules.
8.1.1.1  Effective Non-Freeness Rules. The contextless (obtained by replacing '𝛾' with '⊤' ) forms of rules 1 through 10 define *grammatical* non-freeness (the typical textbook definition). This type of non-freeness is always decidable and can be determined from syntax alone for any WFF not containing term or WFF metavariables. *Effective* non-freeness can be defined by adding the contextless form of rule 11 to rules 1 through 10. This generates an extension of grammatical non-freeness that is conserved through logical equivalence. In the classical semantic case, '𝑥' is *effectively* not free in '𝜑' if and only if every object assignment applied to the variable '𝑥' produces the same truth value in '𝜑'. To be able to make our natural deduction system not just logically equivalent, but *scheme* equivalent to the original Hilbert system, some of the effective non-freeness rules need to be extended to also apply in the *conditional* case. Since it is not always possible to deduce 'Ⅎ𝑥𝜑', given '(𝛾 → Ⅎ𝑥𝜑)', *conditional* non-freeness is an even weaker notion of non-freeness that depends on the given context '𝛾'. As an example consider '𝛾' ≔ '𝑦 = 0' and '𝜑' ≔ '(𝑥 ⋅ 𝑦) = 0'. Then it is true that '(𝛾 → Ⅎ𝑥𝜑)' but 'Ⅎ𝑥𝜑' is not true in general. In other words, '𝑥' is *conditionally* not free in '𝜑' with respect to '𝛾', but '𝑥' is still effectively free in '𝜑' (in the absolute sense). The worked out version of this example is given as example-E7.1a 1074 and example-E7.1b 1075. It also appears that one additional axiom, ndnfrnfr-P7.12 837, is needed to recover the closed form definition of effective non-freeness given in the Hilbert system.
Theorem	ndnfrv-P7.1 826*	Natural Deduction: Effective Non-Freeness Rule 1. If '𝑥' does not occur in '𝜑', then '𝑥' is effectively not free in '𝜑'.
⊢ Ⅎ𝑥𝜑
Theorem	ndnfrneg-P7.2 827	Natural Deduction: Effective Non-Freeness Rule 2. If '𝑥' is (conditionally) effectively not free in '𝜑', then '𝑥' is (conditionally) effectively not free in '¬ 𝜑'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥 ¬ 𝜑)
Theorem	ndnfrim-P7.3 828	Natural Deduction: Effective Non-Freeness Rule 3. If '𝑥' is (conditionally) effectively not free in both '𝜑' and '𝜓', then '𝑥' is (conditionally) effectively not free in '(𝜑 → 𝜓)'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 → 𝜓))
Theorem	ndnfrand-P7.4 829	Natural Deduction: Effective Non-Freeness Rule 4. If '𝑥' is (conditionally) effectively not free in both '𝜑' and '𝜓', then '𝑥' is (conditionally) effectively not free in '(𝜑 ∧ 𝜓)'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ∧ 𝜓))
Theorem	ndnfror-P7.5 830	Natural Deduction: Effective Non-Freeness Rule 5. If '𝑥' is (conditionally) effectively not free in both '𝜑' and '𝜓', then '𝑥' is (conditionally) effectively not free in '(𝜑 ∨ 𝜓)'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ∨ 𝜓))
Theorem	ndnfrbi-P7.6 831	Natural Deduction: Effective Non-Freeness Rule 6. If '𝑥' is (conditionally) effectively not free in both '𝜑' and '𝜓', then '𝑥' is (conditionally) effectively not free in '(𝜑 ↔ 𝜓)'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    &   ⊢ (𝛾 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝛾 → Ⅎ𝑥(𝜑 ↔ 𝜓))
Theorem	ndnfrall1-P7.7 832	Natural Deduction: Effective Non-Freeness Rule 7. '𝑥' is effectively not free in '∀𝑥𝜑' (since any '𝑥' appearing '𝜑' will be bound).
⊢ Ⅎ𝑥∀𝑥𝜑
Theorem	ndnfrex1-P7.8 833	Natural Deduction: Effective Non-Freeness Rule 8. '𝑥' is effectively not free in '∃𝑥𝜑' (since any '𝑥' appearing '𝜑' will be bound).
⊢ Ⅎ𝑥∃𝑥𝜑
Theorem	ndnfrall2-P7.9 834*	Natural Deduction: Effective Non-Freeness Rule 9. If '𝑥' is (conditionally) effectively not free in '𝜑', then '𝑥' is also (conditionally) effectively not free in '∀𝑦𝜑', where '𝑦' is different from '𝑥' and neither '𝑥' nor '𝑦' are effectively free in the context, '𝛾'.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∀𝑦𝜑)
Theorem	ndnfrex2-P7.10 835*	Natural Deduction: Effective Non-Freeness Rule 10. If '𝑥' is (conditionally) effectively not free in '𝜑', then '𝑥' is also (conditionally) effectively not free in '∃𝑦𝜑', where '𝑦' is different from '𝑥' and neither '𝑥' nor '𝑦' are effectively free in the context, '𝛾'.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∃𝑦𝜑)
Theorem	ndnfrleq-P7.11 836	Natural Deduction: Effective Non-Freeness Rule 11. If '𝑥' is not effectively free in the context '𝛾', then the (conditional) effective non-freeness of '𝑥' is conserved between (conditionally) logically equivalent WFFs.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	ndnfrnfr-P7.12 837	Natural Deduction: Effective Non-Freeness Rule 12. The effective non-freeness predicate is itself is effectively not free. In semantic terms, this means that the effective non-freeness of the object variable '𝑥' does not depend on it's value assignment.
⊢ Ⅎ𝑥Ⅎ𝑥𝜑
8.1.1.2  Proper Substitution Rules. These four rules define define all cases where '𝑡' properly replaces '𝑥' in '𝜑'. The first three rules define proper substitution of '𝑡' for '𝑥' when '𝑥' does not occur in '𝑡'. The first rule describes the sufficient condition ("if" part), while the second and third rules together describe the necessary condition ("only if" part). The fourth rule expands the definition of proper substitutioin to include cases where '𝑥' may occur in '𝑡'.
Theorem	ndpsub1-P7.13 838*	Natural Deduction: Proper Substitution Rule 1. '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜓)
Theorem	ndpsub2-P7.14 839*	Natural Deduction: Proper Substitution Rule 2. '𝑥' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ [𝑡 / 𝑥]𝜑))
Theorem	ndpsub3-P7.15 840*	Natural Deduction: Proper Substitution Rule 3. '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥[𝑡 / 𝑥]𝜑
Theorem	ndpsub4-P7.16 841*	Natural Deduction: Proper Substitution Rule 4. '𝑥' can occur in '𝑡', but '𝑦' cannot occur in either '𝜑' or '𝑡'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑦][𝑦 / 𝑥]𝜑)
8.1.1.3  Quantifier Rules. These are the classic introduction and elimination rules for '∀' and '∃'. Effective non-freeness and proper substitution needed to be defined precisely with the previous 12 rules in order to be able to state these next 4 rules.
Theorem	ndalli-P7.17 842*	Natural Deduction: '∀' Introduction Rule. In the traditional textbook presentation '[𝑦 / 𝑥]𝜑' and '𝜑' are written as '𝜑(𝑦)' and '𝜑(𝑥)', respectively. The rule is then stated as... '⊢ (𝛾 → 𝜑(𝑦))   ⇒   ⊢ (𝛾 → ∀𝑥𝜑(𝑥))', where '𝑦' cannot occur free in '𝛾' (that '𝑦' does not occur free in '𝜑(𝑥)' is implied by the notation). The English interpetation of this rule is as follows -- if we can duduce '𝜑(𝑦)' for a specific, but *arbitrary*, '𝑦', then we can deduce that '𝜑(𝑥)' for *any* '𝑥'. To guarantee that '𝑦' is *arbitrary*, '𝑦' must not occur free in '𝛾' (the list of assumptions from which '𝜑(𝑦)' was deduced). Within a proof, the invocation of this rule is often indicated by the use of the phrase "without loss of generality".
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → [𝑦 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	ndalle-P7.18 843	Natural Deduction: '∀' Elimination Rule. In the traditional textbook presentation '𝜑' and '[𝑡 / 𝑥]𝜑' are written as '𝜑(𝑥)' and '𝜑(𝑡)', respectively. The rule is then stated as... '⊢ (𝛾 → ∀𝑥𝜑(𝑥))   ⇒   ⊢ (𝛾 → 𝜑(𝑡))'. The English interpretation of this rule is as follows -- since '𝜑(𝑥)' is true for *any* '𝑥', *in particular*, it is true for '𝑡', thus we can deduce '𝜑(𝑡)'. Within a proof, the phrase "in particular" is a good clue that this rule is being used.
⊢ (𝛾 → ∀𝑥𝜑)    ⇒   ⊢ (𝛾 → [𝑡 / 𝑥]𝜑)
Theorem	ndexi-P7.19 844	Natural Deduction: '∃' Introduction Rule. In the traditional textbook presentation, '[𝑡 / 𝑥]𝜑' and '𝜑' are written as '𝜑(𝑡)' and '𝜑(𝑥)', respectively. The rule is then stated as... '⊢ (𝛾 → 𝜑(𝑡))   ⇒   ⊢ (𝛾 → ∃𝑥𝜑(𝑥))'. Within a proof, this rule is used to replace a specific constant or functional term with an abstract variable. The use of this rule is indicated by the phrase "therefore there exists".
⊢ (𝛾 → [𝑡 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∃𝑥𝜑)
Theorem	ndexe-P7.20 845*	Natural Deduction: '∃' Elimination Rule. In the traditional textbook presentation '[𝑦 / 𝑥]𝜑' and '𝜑' are written as '𝜑(𝑦)' and '𝜑(𝑥)', respectively. The rule is then stated as... '⊢ (𝛾 → (𝜑(𝑦) → 𝜓))   &   ⊢ (𝛾 → ∃𝑥𝜑(𝑥))   ⇒   ⊢ (𝛾 → 𝜓)', where '𝑦' cannot occur free in either '𝛾' or '𝜓' (that '𝑦' does not occur free in '𝜑(𝑥)' is implied by the notation). The English interpretation of this rule is not as straighforward as the previous rules. In a typical proof, one will encounter a statement "let '𝑦' be a something such that '𝜑(𝑦)'" and then go on to deduce '𝜓' over several lines as a sub-proof. To be rigorous, the Deduction Theorem needs to be used to obtain '(𝜑(𝑦) → 𝜓)'. However, in most informal proofs the statement '(𝜑(𝑦) → 𝜓)' is omitted. Instead, the sub-proof is immediately preceeded by the statement that an '𝑥' such that '𝜑(𝑥)' has been shown to exist, invoking the second hypothesis. '𝜓' is then stated as the conclusion, immediately after the subproof. Typically, a sub-proof beginning with "let" is an indication that this rule will be used (at the conclusion of the sub-proof). As for the non-freeness condition, that '𝑦' should not occur free in the context, '𝛾', is clear from the fact that '𝑦' is declared using the word "let", which indicates that '𝑦' is a new variable. That '𝑦' should not occur free in the conclusion '𝜓' is clear from the fact that this rule is used to discharch any statement referencing the temporary variable '𝑦'. In metamath, to avoid using the Deduction Theorem, the assumptions necessary for the sub-proof are simply added to the context (list of assumptions on the left side of the sequent indicated by '𝛾'). This is where temporary variables normally associated with a "let" statement will appear. Such temporary variables are later discharged by invoking this rule. One thing slightly different here is the the third non-freeness hypothesis. Only *conditional* non-freeness of '𝑦' in '𝜒', where '𝛾' is the condition, is necessary. This makes the rule slightly stronger than if we required the stronger hypothesis, '⊢ Ⅎ𝑦𝜓'. This slight strengthing seems to be necessary to deduce the closed form '(Ⅎ𝑥 → (𝜑 → ∀𝑥𝜑))'. The weaker form, given by ndexew-P7 867, is more typically used however.
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → Ⅎ𝑦𝜓)    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
8.1.1.4  Equality Introduction Axiom. The '=' introduction rule serves a similar role as ax-L6 18 in the Hilbert system.
Theorem	ndeqi-P7.21 846	Natural Deduction: '=' Introduction Axiom.
⊢ 𝑡 = 𝑡
8.1.1.5  Substitution Rules (Equality Elimination). In classical texts, all of these rules are often combined into one "substitution" rule that states that if '𝑥 = 𝑡' then '𝑥' can be properly replaced with '𝑡' any place it occurs free. It's impossible to state this general of a scheme in metamath, so we replace it with finite set of rules that, taken together, cover every predicate (indluding equality) and every primitive function in the language. These rules can be combined with other derived substitution laws to obtain the same results.
Theorem	ndsubeql-P7.22a 847	Natural Deduction: Equality Substitution Rule (left).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 = 𝑤 ↔ 𝑢 = 𝑤))
Theorem	ndsubeqr-P7.22b 848	Natural Deduction: Equality Substitution Rule (right).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 = 𝑡 ↔ 𝑤 = 𝑢))
Theorem	ndsubelofl-P7.23a 849	Natural Deduction: Predicate Substitution Rule ('∈' left).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 ∈ 𝑤 ↔ 𝑢 ∈ 𝑤))
Theorem	ndsubelofr-P7.23b 850	Natural Deduction: Predicate Substitution Rule ('∈' right).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑢))
Theorem	ndsubsucc-P7.24a 851	Natural Deduction: Function Substitution Rule ('s‘').
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → s‘𝑡 = s‘𝑢)
Theorem	ndsubaddl-P7.24b 852	Natural Deduction: Function Substitution Rule ('+' left).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 + 𝑤) = (𝑢 + 𝑤))
Theorem	ndsubaddr-P7.24c 853	Natural Deduction: Function Substitution Rule ('+' right).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 + 𝑡) = (𝑤 + 𝑢))
Theorem	ndsubmultl-P7.24d 854	Natural Deduction: Function Substitution Rule ('⋅' left).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))
Theorem	ndsubmultr-P7.24e 855	Natural Deduction: Function Substitution Rule ('⋅' right).
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → (𝑤 ⋅ 𝑡) = (𝑤 ⋅ 𝑢))
8.1.2  Derived Utility Rules. From here on we will treat P3.1 - P3.20 and P7.1 - P7.24 as the new set of axioms. We will no longer refer to any results from chapters 1, 2, 5, or 6 (except indirectly through the axioms stated above). This will allow us to track the us of ndexclmid-P3.16 181. By avoiding the Law of Excluded Middle, it is possible to develop an intuitionist logical framework alongside the standard classical case. From here on, all theorems derived without reference to the Law of Excluded Middle (ndexclmid-P3.16 181) will have a † in the comment.
8.1.2.1  Dual Substitution Rules.
Theorem	ndsubeqd-P7 856	Natural Deduction: Equality Substitution Rule (dual). †
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 = 𝑢 ↔ 𝑡 = 𝑤))
Theorem	ndsubelofd-P7 857	Natural Deduction: Predicate Substitution Rule ('∈' dual). †
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 ∈ 𝑢 ↔ 𝑡 ∈ 𝑤))
Theorem	ndsubaddd-P7 858	Natural Deduction: Function Substitution Rule ('+' dual). †
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 + 𝑢) = (𝑡 + 𝑤))
Theorem	ndsubmultd-P7 859	Natural Deduction: Function Substitution Rule ('⋅' dual). †
⊢ (𝛾 → 𝑠 = 𝑡)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → (𝑠 ⋅ 𝑢) = (𝑡 ⋅ 𝑤))
8.1.2.2  Restricted Variable Forms of Natural Deduction Rules.
Theorem	ndnfrall2-P7.9.VR12of2 860*	ndnfrall2-P7.9 834 with 2 variable restrictions. † Neither '𝑥' nor '𝑦' can occur in '𝛾'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∀𝑦𝜑)
Theorem	ndnfrex2-P7.10.VR12of2 861*	ndnfrex2-P7.10 835 with 2 variable restrictions. † Neither '𝑥' nor '𝑦' can occur in '𝛾'.
⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → Ⅎ𝑥∃𝑦𝜑)
Theorem	ndnfrleq-P7.11.VR 862*	ndnfrleq-P7.11 836 with variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	ndpsub1-P7.13.VR 863*	ndpsub1-P7.13 838 with extra variable restriction. † '𝑥' cannot occur in either '𝑡' or '𝜓'.
⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜓)
Theorem	ndalli-P7.17.VR1of2 864*	ndalli-P7.17 842 with one variable restriction. † '𝑦' cannot occur in '𝛾'.
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → [𝑦 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	ndalli-P7.17.VR2of2 865*	ndalli-P7.17 842 with one variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → [𝑦 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	ndalli-P7.17.VR12of2 866*	ndalli-P7.17 842 with two variable restrictions. † '𝑦' cannot occur in either '𝛾' or '𝜑'.
⊢ (𝛾 → [𝑦 / 𝑥]𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	ndexew-P7 867*	ndexe-P7.20 845 with '𝑦' ENF in '𝜓'. † In the original '∃' Elimination Law, '𝑦' need only be *conditionally* ENF, i.e. '(𝛾 → Ⅎ𝑦𝜓)'.
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR1of3 868*	ndexew-P7 867 with one variable restriction. † '𝑦' cannot occur in '𝛾'.
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR2of3 869*	ndexew-P7 867 with one variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR3of3 870*	ndexew-P7 867 with one variable restriction. † '𝑦' cannot occur in '𝜓'
⊢ Ⅎ𝑦𝛾    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR12of3 871*	ndexew-P7 867 with two variable restrictions. † '𝑦' cannot occur in either '𝛾' or '𝜑'.
⊢ Ⅎ𝑦𝜓    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR13of3 872*	ndexew-P7 867 with two variable restrictions. † '𝑦' cannot occur in either '𝛾' or '𝜓'.
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR23of3 873*	ndexew-P7 867 with two variable restrictions. † '𝑦' cannot occur in either '𝜑' or '𝜓'.
⊢ Ⅎ𝑦𝛾    &   ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndexew-P7.VR123of3 874*	ndexew-P7 867 with three variable restrictions. † '𝑦' cannot occur in '𝛾', '𝜑', or '𝜓'.
⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
8.1.2.3  Inference Forms of Natural Deduction Rules.
Theorem	ndnfrneg-P7.2.RC 875	Inference Form of ndnfrneg-P7.2 827.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥 ¬ 𝜑
Theorem	ndnfrim-P7.3.RC 876	Inference Form of ndnfrim-P7.3 828. †
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 → 𝜓)
Theorem	ndnfrand-P7.4.RC 877	Inference Form of ndnfrand-P7.4 829. †
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓)
Theorem	ndnfror-P7.5.RC 878	Inference Form of ndnfror-P7.5 830. †
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓)
Theorem	ndnfrbi-P7.6.RC 879	Inference Form of ndnfrbi-P7.6 831.
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓)
Theorem	ndnfrall2-P7.9.RC 880*	Inference Form of ndnfrall2-P7.9 834.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	ndnfrex2-P7.10.RC 881*	Inference Form of ndnfrex2-P7.10 835.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	ndnfrleq-P7.11.RC 882	Inference Form of ndnfrleq-P7.11 836. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
Theorem	ndalli-P7.17.RC 883*	Inference form of ndalli-P7.17 842. †
⊢ Ⅎ𝑦𝜑    &   ⊢ [𝑦 / 𝑥]𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	ndalli-P7.17.RC.VR 884*	ndalli-P7.17.RC 883 with variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ [𝑦 / 𝑥]𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	ndalle-P7.18.RC 885	Inference Form of ndalle-P7.18 843. †
⊢ ∀𝑥𝜑    ⇒   ⊢ [𝑡 / 𝑥]𝜑
Theorem	ndexi-P7.19.RC 886	Inference Form of ndexi-P7.19 844. †
⊢ [𝑡 / 𝑥]𝜑    ⇒   ⊢ ∃𝑥𝜑
Theorem	ndexew-P7.RC 887*	Inference Form of ndexew-P7 867. †
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ndexew-P7.RC.VR1of2 888*	ndexew-P7.RC 887 with one variable restriction. † '𝑦' cannot occur in '𝜑'.
⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ndexew-P7.RC.VR2of2 889*	ndexew-P7.RC 887 with one variable restriction. † '𝑦' cannot occur in '𝜓'.
⊢ Ⅎ𝑦𝜑    &   ⊢ ([𝑦 / 𝑥]𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ndexew-P7.RC.VR12of2 890*	ndexew-P7.RC 887 with two variable restrictions. † '𝑦' cannot occur in either '𝜑' or '𝜓'.
⊢ ([𝑦 / 𝑥]𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ndsubeql-P7.22a.RC 891	Inference Form of ndsubeql-P7.22a 847. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑡 = 𝑤 ↔ 𝑢 = 𝑤)
Theorem	ndsubeqr-P7.22b.RC 892	Inference Form of ndsubeqr-P7.22b 848. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑤 = 𝑡 ↔ 𝑤 = 𝑢)
Theorem	ndsubeqd-P7.RC 893	Inference Form of ndsubeqd-P7 856. †
⊢ 𝑠 = 𝑡    &   ⊢ 𝑢 = 𝑤    ⇒   ⊢ (𝑠 = 𝑢 ↔ 𝑡 = 𝑤)
Theorem	ndsubelofl-P7.23a.RC 894	Inference Form of ndsubelofl-P7.23a 849. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑡 ∈ 𝑤 ↔ 𝑢 ∈ 𝑤)
Theorem	ndsubelofr-P7.23b.RC 895	Inference Form of ndsubelofr-P7.23b 850. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑢)
Theorem	ndsubelofd-P7.RC 896	Inference Form of ndsubelofd-P7 857. †
⊢ 𝑠 = 𝑡    &   ⊢ 𝑢 = 𝑤    ⇒   ⊢ (𝑠 ∈ 𝑢 ↔ 𝑡 ∈ 𝑤)
Theorem	ndsubsucc-P7.24a.RC 897	Inference Form of ndsubsucc-P7.24a 851. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ s‘𝑡 = s‘𝑢
Theorem	ndsubaddl-P7.24b.RC 898	Inference Form of ndsubaddl-P7.24b 852. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑡 + 𝑤) = (𝑢 + 𝑤)
Theorem	ndsubaddr-P7.24c.RC 899	Inference Form of ndsubaddr-P7.24c 853. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑤 + 𝑡) = (𝑤 + 𝑢)
Theorem	ndsubaddd-P7.RC 900	Inference Form of ndsubaddd-P7 858. †
⊢ 𝑠 = 𝑡    &   ⊢ 𝑢 = 𝑤    ⇒   ⊢ (𝑠 + 𝑢) = (𝑡 + 𝑤)