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

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

Type	Label	Description
Statement
3.2  Logical Equivalence
3.2.1  Motivation Theorems. If we use 'equiv(𝜑, 𝜓)' as an abbreviation for '¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))', then it follows from lemmas mbifwd-P2.1a 101, mbirev-P2.1b 102, and mbicmb-P2.1c 103 that... ⊢ equiv(𝜑, 𝜓) ⇔ ⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜑). This proves that the formula 'equiv(𝜑, 𝜓) ≔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))' precisely represents the property of logical equivalence between '𝜑' and '𝜓'. We can use this to our advantage in order to define '(𝜑 ↔ 𝜓)'.
Theorem	mbifwd-P2.1a 101	Motivation for ↔ Definition, Part A.
⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	mbirev-P2.1b 102	Motivation for ↔ Definition, Part B.
⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	mbicmb-P2.1c 103	Motivation for ↔ Definition, Part C.
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))
3.2.2  Defining Logical Equivalence. While it would be tempting to write '⊢ ((𝜑 ↔ 𝜓) ↔ equiv(𝜑, 𝜓))' as the definition of '↔' , nested occurances of the root symbol being introduced should not appear in a definition. We instead use... ⊢ equiv((𝜑 ↔ 𝜓), equiv(𝜑, 𝜓)). Without the help of the abbreviation, this definitional expression is complex and difficult to read. However, it is simply a nested application of the formula denoted by 'equiv', which we have already shown is synonymous with logical equivalence.
3.2.2.1  Syntax Definition.
Syntax	wff-bi 104	Extend WFF definition to include the biconditional symbol '↔'.
wff (𝜑 ↔ 𝜓)
3.2.2.2  Justification Theorem. We will later use the theorem bijust-P2.2 106 as an aid the semantic proof that this definition conservatively extends the system using the original 9 FOL axioms. The theorem is just the definition... ⊢ equiv((𝜑 ↔ 𝜓), equiv(𝜑, 𝜓) ), with 'equiv(𝜑, 𝜓)' substituted for '(𝜑 ↔ 𝜓)'. That is... ⊢ equiv( equiv(𝜑, 𝜓), equiv(𝜑, 𝜓) ). This is just a special case of the statement... ⊢ equiv(𝛾, 𝛾), which is proven as bijust-P2.2-L1 105.
Theorem	bijust-P2.2-L1 105	Lemma for bijust-P2.2 106. [Auxiliary lemma - not displayed.]
Theorem	bijust-P2.2 106	Justification Theorem for df-bi-D2.1 107.
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3.2.2.3  Formal Definition.
Definition	df-bi-D2.1 107	Definition of Biconditional, '↔'. Read as "if and only if".
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
3.2.2.4  Standard Form. We now derive the "if" (dfbiif-P2.3a 108) and "only if" (dfbionlyif-P2.3b 109) parts of the statement that '(𝜑 ↔ 𝜓)' is equivalent to 'eq(𝜑, 𝜓)'. Taken together with the various substitution properties of '↔' which we will prove later, the theorems dfbiif-P2.3a 108, and dfbionlyif-P2.3b 109 can be used to show that the ↔ symbol is always eliminable. Finally, we combine the previous statement into one in the form of dfbialt-P2.4 110. This can be thought of as the standard form of the definition which follows the typical idiom... definiendum '↔' definiens.
Theorem	dfbiif-P2.3a 108	Sufficient Conditon for (i.e. "If" part of) df-bi-D2.1 107.
⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
Theorem	dfbionlyif-P2.3b 109	Necessary Condition for (i.e. "Only If" part of) df-bi-D2.1 107.
⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
Theorem	dfbialt-P2.4 110	Alternate Form of df-bi-D2.1 107.
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3.2.3  Fundamental Properties. Taken together, the properties bifwd-P2.5a 111, birev-P2.5b 115, and bicmb-P2.5c 119 completely define logical equivalence.
Theorem	bifwd-P2.5a 111	'↔' Forward Implication.
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
Theorem	bifwd-P2.5a.SH 112	Inference from bifwd-P2.5a 111.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	bifwd-P2.5a.AC.SH 113	Deductive Form of bifwd-P2.5a 111
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜓))
Theorem	bifwd-P2.5a.2AC.SH 114	Another Deductive form of bifwd-P2.5a 111.
⊢ (𝛾₁ → (𝛾₂ → (𝜑 ↔ 𝜓)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝜑 → 𝜓)))
Theorem	birev-P2.5b 115	'↔' Reverse Implication.
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
Theorem	birev-P2.5b.SH 116	Inference from birev-P2.5b 115.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	birev-P2.5b.AC.SH 117	Deductive Form of birev-P2.5b 115
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	birev-P2.5b.2AC.SH 118	Another Deductive Form of birev-P2.5b 115
⊢ (𝛾₁ → (𝛾₂ → (𝜑 ↔ 𝜓)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝜓 → 𝜑)))
Theorem	bicmb-P2.5c 119	'↔' Combine Implications.
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
Theorem	bicmb-P2.5c.2SH 120	Inference from bicmb-P2.5c 119.
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	bicmb-P2.5c.AC.2SH 121	Deductive Form of bicmb-P2.5c 119.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜑))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜓))
Theorem	bicmb-P2.5c.2AC.2SH 122	Another Deductive Form of bicmb-P2.5c 119.
⊢ (𝛾₁ → (𝛾₂ → (𝜑 → 𝜓)))    &   ⊢ (𝛾₁ → (𝛾₂ → (𝜓 → 𝜑)))    ⇒   ⊢ (𝛾₁ → (𝛾₂ → (𝜑 ↔ 𝜓)))
3.2.4  Equivalence Relation Properties. Show that '↔' is an equivalence relation.
Theorem	biref-P2.6a 123	Equivalence Property: '↔' Reflexivity.
⊢ (𝜑 ↔ 𝜑)
Theorem	bisym-P2.6b 124	Equivalence Property: '↔' Symmetry.
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	bisym-P2.6b.SH 125	Inference from bisym-P2.6b 124.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ↔ 𝜑)
Theorem	bitrns-P2.6c 126	Equivalence Property: '↔' Transitivity.
⊢ ((𝜑 ↔ 𝜓) → ((𝜓 ↔ 𝜒) → (𝜑 ↔ 𝜒)))
3.2.5  Substitution Laws. These laws can be chained together to produce a countably infinite set of rules of the form... ((𝜑 ↔ 𝜓) → (𝜗 ↔ 𝜗(𝜓/𝜑)), where '𝜗' involves some combination of connectives '¬' and '→', and contains the sub-formula '𝜑'. The notation '𝜗(𝜓/𝜑)' indicates the formula '𝜗' with one or more instances of the sub-formula '𝜑' replaced with '𝜓'. This idea will be expanded to formulas with quantifiers after developing the rules of predicate calculus.
Theorem	subneg-P2.7 127	Substitution Law for '¬'.
⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
Theorem	subiml-P2.8a 128	Left Substitution Law for '→'.
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
Theorem	subiml-P2.8a.SH 129	Inference from subiml-P2.8a 128.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))
Theorem	subimr-P2.8b 130	Right Substitution Law for '→'.
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
Theorem	subimr-P2.8b.SH 131	Inference from subimr-P2.8b 130.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))
3.3  Logical Conjunction
3.3.1  Defining Logical Conjunction.
3.3.1.1  Syntax Definition.
Syntax	wff-and 132	Extend WFF definition to include the "and" symbol '∧'.
wff (𝜑 ∧ 𝜓)
3.3.1.2  Formal Definition.
Definition	df-and-D2.2 133	Definition of Conjunction, '∧'. Read as "and".
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
3.3.2  Fundamental Properties. Taken together, the properties simpl-P2.9a 134, simpr-P2.9b 136, and cmb-P2.9c 138 completely define logical conjunction.
Theorem	simpl-P2.9a 134	'∧' Left Simplification.
⊢ ((𝜑 ∧ 𝜓) → 𝜑)
Theorem	simpl-P2.9a.AC.SH 135	Deductive Form of simpl-P2.9a 134.
⊢ (𝛾 → (𝜑 ∧ 𝜓))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	simpr-P2.9b 136	'∧' Right Simplification.
⊢ ((𝜑 ∧ 𝜓) → 𝜓)
Theorem	simpr-P2.9b.AC.SH 137	Deductive Form of simpr-P2.9b 136.
⊢ (𝛾 → (𝜑 ∧ 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	cmb-P2.9c 138	'∧' Introduction by Combination.
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
Theorem	cmb-P2.9c.AC.2SH 139	Deductive Form of cmb-P2.9c 138.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → 𝜓)    ⇒   ⊢ (𝛾 → (𝜑 ∧ 𝜓))
3.3.3  Importation and Exportation Laws.
Theorem	import-P2.10a 140	'∧' Importation Law.
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	import-P2.10a.SH 141	Inference from import-P2.10a 140.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	export-P2.10b 142	'∧' Exportation Law.
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	export-P2.10b.SH 143	Inference from export-P2.10b 142.
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
3.4  Logical Disjunction
3.4.1  Defining Logical Disjunction.
3.4.1.1  Syntax Definition.
Syntax	wff-or 144	Extend WFF definition to include the "or" symbol '∨'.
wff (𝜑 ∨ 𝜓)
3.4.1.2  Formal Definition.
Definition	df-or-D2.3 145	Definition of Disjunction, '∨'. Read as "or".
⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3.4.2  Fundamental Properties. Taken together, the properties orintl-P2.11a 146, orintr-P2.11b 148, and orelim-P2.11c 150 completely define logical disjunction.
Theorem	orintl-P2.11a 146	Left Introduction Rule for '∨'.
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	orintl-P2.11a.AC.SH 147	Deductive Form of orintl-P2.11a 146.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜓 ∨ 𝜑))
Theorem	orintr-P2.11b 148	Right Introduction Rule for '∨'.
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	orintr-P2.11b.AC.SH 149	Deductive Form of orintr-P2.11b 148.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜑 ∨ 𝜓))
Theorem	orelim-P2.11c 150	'∧' Elimination Law. This is also known as the "Proof by Cases" law.
⊢ ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → 𝜒)))
Theorem	orelim-P2.11c.AC.3SH 151	Deductive Form of orelim-P2.11c 150.
⊢ (𝛾 → (𝜑 → 𝜒))    &   ⊢ (𝛾 → (𝜓 → 𝜒))    &   ⊢ (𝛾 → (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾 → 𝜒)
3.4.3  The Law of Excluded Middle.
Theorem	exclmid-P2.12 152	Law of Excluded Middle.
⊢ (𝜑 ∨ ¬ 𝜑)
3.5  True and False Constants.
3.5.1  Defining True.
3.5.1.1  Syntax Definition.
Syntax	wff-true 153	Extend WFF definition to include the "true" constant '⊤'.
wff ⊤
3.5.1.2  Justification Theorem.
Theorem	truejust-P2.13 154	Justification Theorem for df-true-D2.4 155.
⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) ↔ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦))
3.5.1.3  Formal Definition.
Definition	df-true-D2.4 155	Definition of True, '⊤'.
⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3.5.2  Fundamental Property of "True" Constant.
Theorem	true-P2.14 156	'⊤' is a theorem.
⊢ ⊤
3.5.3  Defining False.
3.5.3.1  Syntax Definition.
Syntax	wff-false 157	Extend WFF definition to include the "false" constant '⊥'.
wff ⊥
3.5.3.2  Formal Definition.
Definition	df-false-D2.5 158	Definition of False, '⊥'.
⊢ (⊥ ↔ ¬ ⊤)
3.5.4  Fundamental Property of "False" Constant.
Theorem	false-P2.15 159	'⊥' is refutable.
⊢ ¬ ⊥
PART 4  Chapter 3: Propositional Calculus (Natural Deduction)
4.1  Define Conjunction Tuples.
Syntax	wff-rcp-AND3 160	Extend WFF definition to include '∧' 3-Tuple.
wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃)
Definition	df-rcp-AND3 161	'∧' 3-Tuple.
⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃) ↔ ((𝜑₁ ∧ 𝜑₂) ∧ 𝜑₃))
Syntax	wff-rcp-AND4 162	Extend WFF definition to include '∧' 4-Tuple.
wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄)
Definition	df-rcp-AND4 163	'∧' 4-Tuple.
⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ↔ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃) ∧ 𝜑₄))
Syntax	wff-rcp-AND5 164	Extend WFF definition to include '∧' 5-Tuple.
wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅)
Definition	df-rcp-AND5 165	'∧' 5-Tuple.
⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅) ↔ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄) ∧ 𝜑₅))
4.2  Natural Deduction for Propositional Calculus. These rules introduce a new axiomatic system designed to emulate natural deduction using Gentzen sequent notation. Lines are writen as... (𝛾 → 𝜑), to emulate the sequent notation... 𝛾 ⊢ 𝜑. '𝛾' can be understood as a list of assumptions. Here we write ((𝛾₁ ∧ 𝛾₂ ∧... 𝛾n ) → 𝜑), to emulate... 𝛾₁, 𝛾₂, ... , 𝛾n ⊢ 𝜑. Rule 1 is used to emulate the statement (or re-statement) of an assumption (i.e. a formula on the left hand side), and rule 2 is used to import an earlier result into a new context with additional assumptions (i.e. additional formulas on the left hand side). Either of these two rules can be used to emulate the introduction of a new assumptions. Rules 3, 5, and 12 are used emulate the discharging of assumptions. The one limitation of our notation is the inability to express the case where the left side of the sequent is empty. To facilitate this we must introduce the symbol '⊤' along with two additional rules (17 and 18) for its introduction and elimination. We can then replace '𝛾' with '⊤' and use any of the rules 1 - 15 as normal. Rules 19 and 20 introduce and eliminate the the corresponding '⊥' symbol. This symbol isn't strictly necessary, but serves for more convenient and standard notation when doing natural deduction proofs by contradiction. Rule 3 would usually be used to introduce '⊥', but the redundant rule 19 is included as the corresponding dual form of the '⊤' rule. In our syntax... (𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧... 𝛾n ) is shorthand for... (... ((𝛾₁ ∧ 𝛾₂) ∧ 𝛾₃)... 𝛾n ). This syntax allows one to write sequents of length longer than three without the need for nested parentheses. The recipes 'rcp-NDSEP' and 'rcp-NDJOIN' facilitate the use of this syntax. Addational versions can be added as needed for longer sequents. These rules merely add more convenient syntax. They do not extend the logic at all.
4.2.1  Axiomatic Rules.
Theorem	ndasm-P3.1 166	Natural Deduction: State Assumption. This rule is simply stating an assumption.
⊢ ((𝛾 ∧ 𝜑) → 𝜑)
Theorem	ndimp-P3.2 167	Natural Deduction: Import Previous Consequent. Any previous consequent can be re-stated with an additional assumption added.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ ((𝛾 ∧ 𝜓) → 𝜑)
Theorem	ndnegi-P3.3 168	Natural Deduction: '¬' Introduction Rule. If an assumption leads to a contradiction, then we can discharge it and conclude its negation.
⊢ ((𝛾 ∧ 𝜑) → 𝜓)    &   ⊢ ((𝛾 ∧ 𝜑) → ¬ 𝜓)    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	ndnege-P3.4 169	Natural Deduction: '¬' Elimination Rule. If we can deduce a contradiction within some context, then we can deduce any arbitrary WFF from that same context.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndimi-P3.5 170	Natural Deduction: '→' Introduction Rule. If we can deduce '𝜓' after assuming '𝜑', then we can conclude '𝜑 → 𝜓' with '𝜑' discharged.
⊢ ((𝛾 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝛾 → (𝜑 → 𝜓))
Theorem	ndime-P3.6 171	Natural Deduction: '→' Elimination Rule. This rule is just Modus Ponens with an added context.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndandi-P3.7 172	Natural Deduction: '∧' Introduction Rule. Deduce the conjunction of two previously deduced WFFs.
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → 𝜓)    ⇒   ⊢ (𝛾 → (𝜑 ∧ 𝜓))
Theorem	ndandel-P3.8 173	Natural Deduction: Left '∧' Elimination Rule. Deduce the right conjunct (i.e. eliminate the left conjunct) of a previously deduced conjunction.
⊢ (𝛾 → (𝜑 ∧ 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	ndander-P3.9 174	Natural Deduction: Right '∧' Elimination Rule. Deduce the left conjunct (i.e. eliminate the right conjunct) of a previously deduced conjunction.
⊢ (𝛾 → (𝜑 ∧ 𝜓))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	ndoril-P3.10 175	Natural Deduction: Left '∨' Introduction Rule. Deduce a new disjunction containing an arbitrary WFF to the left of a previously deduced WFF.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜓 ∨ 𝜑))
Theorem	ndorir-P3.11 176	Natural Deduction: Right '∨' Introduction Rule. Deduce a new disjunction containing an arbitrary WFF to the right of a previously deduced WFF.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜑 ∨ 𝜓))
Theorem	ndore-P3.12 177	Natural Deduction: '∨' Elimination Rule. If... 1.) after assuming '𝜑' we deduce '𝜒', 2.) after assuming '𝜓' we also deduce '𝜒', and 3.) we know that either '𝜑' or '𝜓' holds, then we can deduce '𝜒' with the case assumptions, '𝜑' and '𝜓', discharged.
⊢ ((𝛾 ∧ 𝜑) → 𝜒)    &   ⊢ ((𝛾 ∧ 𝜓) → 𝜒)    &   ⊢ (𝛾 → (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾 → 𝜒)
Theorem	ndbii-P3.13 178	Natural Deduction: '↔' Introduction Rule. If we have previously deduced both directions of a biconditional, then we can deduce the full biconditional.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜑))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜓))
Theorem	ndbief-P3.14 179	Natural Deduction: '↔' Elimination Rule - Forward Implication. After deducing a biconditional statement, we can deduce the assocated forward implication.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜓))
Theorem	ndbier-P3.15 180	Natural Deduction: '↔' Elimination Rule - Reverse Implication. After deducing a biconditional statement, we can deduce the associated reverse implication.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	ndexclmid-P3.16 181	Natural Deduction: Law of Excluded Middle (restated). Every WFF '𝜑' is either true or false. This law is rejected within intuitionist logic.
⊢ (𝜑 ∨ ¬ 𝜑)
4.2.1.1  Rules for "True" and "False" Constants.
Theorem	ndtruei-P3.17 182	Natural Deduction: '⊤' Introduction Rule. This can be used to turn an ordinary theorem into a sequent. In this case '⊤' represents '𝛾' and any of the rules 1 - 15 can be applied.
⊢ 𝜑    ⇒   ⊢ (⊤ → 𝜑)
Theorem	ndtruee-P3.18 183	Natural Deduction: '⊤' Elimination Rule. Rules 17 and 18 allow us to write '(⊤ → 𝜑)' as a synonym for stating "'𝜑' is true" (or, more precisely, deducable).
⊢ (⊤ → 𝜑)    ⇒   ⊢ 𝜑
Theorem	ndfalsei-P3.19 184	Natural Deduction: '⊥' Introduction Rule. This statement can be proved from ndasm-P3.1 166, ndimp-P3.2 167, ndimi-P3.5 170, ndnege-P3.4 169, ndtruei-P3.17 182, and ndtruee-P3.18 183. It's included to keep the pattern of having an introduction rule to go along with every elimination rule. ndtruei-P3.17 182 would normally be redundant as well, but it is needed to facilitate the contextless cases not covered by rules 1 - 15.
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 → ⊥)
Theorem	ndfalsee-P3.20 185	Natural Deduction: '⊥' Elimination Rule. Rules 19 and 20 allow us to write '(𝜑 → ⊥)' as a synonym for "'𝜑' is false" (or, more precisely, refutable).
⊢ (𝜑 → ⊥)    ⇒   ⊢ ¬ 𝜑
4.2.1.2  Separate Front Supposition (Syntactic Axioms). This recipe is used in conjunction with ndnegi-P3.3 168, ndimi-P3.5 170, and ndore-P3.12 177.
Theorem	rcp-NDSEP3 186	( 1 ∧ 2 ∧ 3 ) ⇒ ( ( 1 ∧ 2 ) ∧ 3 ).
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)    ⇒   ⊢ (((𝛾₁ ∧ 𝛾₂) ∧ 𝛾₃) → 𝜑)
Theorem	rcp-NDSEP4 187	( 1 ∧ 2 ∧ 3 ∧ 4 ) ⇒ ( ( 1 ∧ 2 ∧ 3 ) ∧ 4 ).
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)    ⇒   ⊢ (((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) ∧ 𝛾₄) → 𝜑)
Theorem	rcp-NDSEP5 188	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) ⇒ ( ( 1 ∧ 2 ∧ 3 ∧ 4 ) ∧ 5 ).
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)    ⇒   ⊢ (((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) ∧ 𝛾₅) → 𝜑)
4.2.1.3  Join Front Supposition (Syntactic Axioms). This recipe is used in conjunction with ndasm-P3.1 166 and ndimp-P3.2 167.
Theorem	rcp-NDJOIN3 189	( ( 1 ∧ 2 ) ∧ 3 ) ⇒ ( 1 ∧ 2 ∧ 3 ).
⊢ (((𝛾₁ ∧ 𝛾₂) ∧ 𝛾₃) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)
Theorem	rcp-NDJOIN4 190	( ( 1 ∧ 2 ∧ 3 ) ∧ 4 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ).
⊢ (((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) ∧ 𝛾₄) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)
Theorem	rcp-NDJOIN5 191	( ( 1 ∧ 2 ∧ 3 ∧ 4 ) ∧ 5 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ).
⊢ (((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) ∧ 𝛾₅) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)
4.2.2  Utility Recipes. For the rest of the chapter we will treat P3.1 - P3.20 as a new set of axioms. From here on out, we will not rely on any results from chapters 1 or 2 (except indirectly through the new set of axioms). This will allow us to track the use 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.
4.2.2.1  Derived Rules for Stating / Re-Stating Assumptions. These derived rules may be used in place of ndasm-P3.1 166.
Theorem	rcp-NDASM1of1 192	( 1 ) → 1. †
⊢ (𝛾₁ → 𝛾₁)
Theorem	rcp-NDASM1of2 193	( 1 ∧ 2 ) → 1. †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₁)
Theorem	rcp-NDASM2of2 194	( 1 ∧ 2 ) → 2. †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₂)
Theorem	rcp-NDASM1of3 195	( 1 ∧ 2 ∧ 3 ) → 1. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝛾₁)
Theorem	rcp-NDASM2of3 196	( 1 ∧ 2 ∧ 3 ) → 2. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝛾₂)
Theorem	rcp-NDASM3of3 197	( 1 ∧ 2 ∧ 3 ) → 3. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝛾₃)
Theorem	rcp-NDASM1of4 198	( 1 ∧ 2 ∧ 3 ∧ 4 ) → 1. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₁)
Theorem	rcp-NDASM2of4 199	( 1 ∧ 2 ∧ 3 ∧ 4 ) → 2. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₂)
Theorem	rcp-NDASM3of4 200	( 1 ∧ 2 ∧ 3 ∧ 4 ) → 3. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₃)