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

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

Type	Label	Description
Statement
Theorem	rcp-NDASM4of4 201	( 1 ∧ 2 ∧ 3 ∧ 4 ) → 4. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₄)
Theorem	rcp-NDASM1of5 202	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) → 1. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝛾₁)
Theorem	rcp-NDASM2of5 203	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) → 2. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝛾₂)
Theorem	rcp-NDASM3of5 204	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) → 3. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝛾₃)
Theorem	rcp-NDASM4of5 205	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) → 4. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝛾₄)
Theorem	rcp-NDASM5of5 206	( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ) → 5. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝛾₅)
4.2.2.2  Derived Rules for Importing Previous Results. These derived rules may be used in place of ndimp-P3.2 167.
Theorem	rcp-NDIMP0addall 207	( ) ⇒ ( 1 ∧... ∧ n ). †
⊢ 𝜑    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	rcp-NDIMP1add1 208	( 1 ) ⇒ ( 1 ∧ 2 ). †
⊢ (𝛾₁ → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)
Theorem	rcp-NDIMP2add1 209	( 1 ∧ 2 ) ⇒ ( 1 ∧ 2 ∧ 3 ). †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)
Theorem	rcp-NDIMP3add1 210	( 1 ∧ 2 ∧ 3 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ). †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)
Theorem	rcp-NDIMP4add1 211	( 1 ∧ 2 ∧ 3 ∧ 4 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ). †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)
Theorem	rcp-NDIMP1add2 212	( 1 ) ⇒ ( 1 ∧ 2 ∧ 3 ). †
⊢ (𝛾₁ → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)
Theorem	rcp-NDIMP2add2 213	( 1 ∧ 2 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ). †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)
Theorem	rcp-NDIMP3add2 214	( 1 ∧ 2 ∧ 3 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ). †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)
Theorem	rcp-NDIMP1add3 215	( 1 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ). †
⊢ (𝛾₁ → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)
Theorem	rcp-NDIMP2add3 216	( 1 ∧ 2 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ). †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)
Theorem	rcp-NDIMP1add4 217	( 1 ) ⇒ ( 1 ∧ 2 ∧ 3 ∧ 4 ∧ 5 ). †
⊢ (𝛾₁ → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)
4.2.2.3  Derived Rules for Negation Introduction. These derived rules may be used in place of ndnegi-P3.3 168.
Theorem	rcp-NDNEGI1 218	¬ Introduction Recipe. †
⊢ (𝛾₁ → 𝜑)    &   ⊢ (𝛾₁ → ¬ 𝜑)    ⇒   ⊢ ¬ 𝛾₁
Theorem	rcp-NDNEGI2 219	¬ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂) → ¬ 𝜑)    ⇒   ⊢ (𝛾₁ → ¬ 𝛾₂)
Theorem	rcp-NDNEGI3 220	¬ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → ¬ 𝛾₃)
Theorem	rcp-NDNEGI4 221	¬ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → ¬ 𝛾₄)
Theorem	rcp-NDNEGI5 222	¬ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → ¬ 𝛾₅)
4.2.2.4  Derived Rule for Negation Elimination. This derived rule is used in place of ndnege-P3.4 169 when '𝛾' is empty.
Theorem	rcp-NDNEGE0 223	This is equivalent to the Principle of Explosion. †
⊢ 𝜑    &   ⊢ ¬ 𝜑    ⇒   ⊢ 𝜓
4.2.2.5  Derived Rules for Implication Introduction. These derived rules may be used in place of ndimi-P3.5 170.
Theorem	rcp-NDIMI2 224	→ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)    ⇒   ⊢ (𝛾₁ → (𝛾₂ → 𝜑))
Theorem	rcp-NDIMI3 225	→ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → (𝛾₃ → 𝜑))
Theorem	rcp-NDIMI4 226	→ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → (𝛾₄ → 𝜑))
Theorem	rcp-NDIMI5 227	→ Introduction Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝛾₅) → 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → (𝛾₅ → 𝜑))
4.2.2.6  Derived Rule for Implication Elimination. This derived rule replaces ndime-P3.6 171 when '𝛾' is empty.
Theorem	rcp-NDIME0 228	This is the same is ax-MP 14. †
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
4.2.2.7  Derived Rule for Conjunction Introduction. This derived rule is used in place of ndandi-P3.7 172 when '𝛾' is empty.
Theorem	rcp-NDANDI0 229	'∧' Introduction. †
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ∧ 𝜓)
4.2.2.8  Derived Rule for Left Conjunction Elimination. This derived rule is used in place of ndandel-P3.8 173 when '𝛾' is empty.
Theorem	rcp-NDANDEL0 230	Left '∧' Elimination. †
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜓
4.2.2.9  Derived Rule for Right Conjunction Elimination. This derived rule is used in place of ndander-P3.9 174 when '𝛾' is empty.
Theorem	rcp-NDANDER0 231	Right '∧' Elimination. †
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜑
4.2.2.10  Derived Rule for Left Disjunction Introduction. This derived rule is used in place of ndoril-P3.10 175 when '𝛾' is empty.
Theorem	rcp-NDORIL0 232	Left '∨' Introduction. †
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑)
4.2.2.11  Derived Rule for Right Disjunction Introduction. This derived rule is used in place of ndorir-P3.11 176 when '𝛾' is empty.
Theorem	rcp-NDORIR0 233	Right '∨' Introduction. †
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓)
4.2.2.12  Derived Rules for Disjunction Elimination These derived rules may be used in place of ndore-P3.12 177.
Theorem	rcp-NDORE1 234	∨ Elimination Recipe. †
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ 𝜒
Theorem	rcp-NDORE2 235	∨ Elimination Recipe. †
⊢ ((𝛾₁ ∧ 𝜑) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝜓) → 𝜒)    &   ⊢ (𝛾₁ → (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾₁ → 𝜒)
Theorem	rcp-NDORE3 236	∨ Elimination Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝜑) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝜓) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂) → (𝜑 ∨ 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜒)
Theorem	rcp-NDORE4 237	∨ Elimination Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝜑) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝜓) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → (𝜑 ∨ 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝜒)
Theorem	rcp-NDORE5 238	∨ Elimination Recipe. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝜑) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝜓) → 𝜒)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → (𝜑 ∨ 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝜒)
4.2.2.13  Derived Rule for Biconditional Introduction. This derived rule is used in place of ndbii-P3.13 178 when '𝛾' is empty.
Theorem	rcp-NDBII0 239	'↔' Introduction. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝜓)
4.2.2.14  Derived Rule for Biconditional Forward Implication. This derived rule is used in place of ndbief-P3.14 179 when '𝛾' is empty.
Theorem	rcp-NDBIEF0 240	'↔' Elimination by Forward Implication Introduction. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
4.2.2.15  Derived Rule for Biconditional Reverse Implication. This derived rule is used in place of ndbier-P3.15 180 when '𝛾' is empty.
Theorem	rcp-NDBIER0 241	'↔' Elimination by Reverse Implication Introduction. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
4.2.3  Closed Forms of Natural Deduction Rules. The closed form of ndimp-P3.2 167 is just the Hilbert Axiom L1, which we deduce later as axL1-P3.21.CL 253. The closed forms of ndimi-P3.5 170 and ndandi-P3.7 172 are trivial cases of implication identity, which is already availible as rcp-NDASM1of1 192. The closed forms of ndandel-P3.8 173 and ndander-P3.9 174 are also already availible as rcp-NDASM1of2 193 and rcp-NDASM2of2 194.
Theorem	ndnegi-P3.3.CL 242	Closed Form of ndnegi-P3.3 168. †
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) → ¬ 𝜑)
Theorem	ndnege-P3.4.CL 243	Closed Form of ndnege-P3.4 169. †
⊢ ((𝜑 ∧ ¬ 𝜑) → 𝜓)
Theorem	ndime-P3.6.CL 244	Closed Form of ndime-P3.6 171. †
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)
Theorem	ndoril-P3.10.CL 245	Closed Form of ndoril-P3.10 175. †
⊢ (𝜑 → (𝜓 ∨ 𝜑))
Theorem	ndorir-P3.11.CL 246	Closed Form of ndorir-P3.11 176. †
⊢ (𝜑 → (𝜑 ∨ 𝜓))
Theorem	ndore-P3.12.CL 247	Closed Form of ndore-P3.12 177. †
⊢ (((𝜑 → 𝜒) ∧ (𝜓 → 𝜒) ∧ (𝜑 ∨ 𝜓)) → 𝜒)
Theorem	ndbii-P3.13.CL 248	Closed Form of ndbii-P3.13 178. †
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
Theorem	ndbief-P3.14.CL 249	Closed Form of ndbief-P3.14 179. †
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
Theorem	ndbier-P3.15.CL 250	Closed Form of ndbier-P3.15 180. †
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
4.2.4  A More Convenient form of Law of Excluded Middle.
Theorem	ndexclmid-P3.16.AC 251	Alternate Form of Excluded Middle.
⊢ (𝛾 → (𝜑 ∨ ¬ 𝜑))
4.3  Revisiting Chapter 1.
4.3.1  Propositional Axioms L1 and L2.
Theorem	axL1-P3.21 252	Re-derived Deductive Form of Axiom L1. †
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	axL1-P3.21.CL 253	Closed Form of axL1-P3.21 252 (Axiom L1). †
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	axL2-P3.22 254	Re-derived Deductive Form of Axiom L2. †
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	axL2-P3.22.RC 255	Inference Form of axL2-P3.22 254. †
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
Theorem	axL2-P3.22.CL 256	Closed Form of axL2-P3.22 254 (Axiom L2). †
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
4.3.2  Other Implication Laws.
Theorem	mae-P3.23 257	Middle Antecedent Elimination. †
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    &   ⊢ (𝛾 → 𝜓)    ⇒   ⊢ (𝛾 → (𝜑 → 𝜒))
Theorem	mae-P3.23.RC 258	Inference Form of mae-P3.23 257. †
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	syl-P3.24 259	Syllogism. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜒))
Theorem	syl-P3.24.RC 260	Inference Form of syl-P3.24.RC 260. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	dsyl-P3.25 261	Double Syllogism. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜓 → 𝜒))    &   ⊢ (𝛾 → (𝜒 → 𝜗))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜗))
Theorem	dsyl-P3.25.RC 262	Inference Form of dsyl-P3.25 261. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜒 → 𝜗)    ⇒   ⊢ (𝜑 → 𝜗)
Theorem	rae-P3.26 263	Redundant Antecedent Elimination. †
⊢ (𝛾 → (𝜑 → (𝜑 → 𝜓)))    ⇒   ⊢ (𝛾 → (𝜑 → 𝜓))
Theorem	rae-P3.26.RC 264	Inference Form of rae-P3.26 263. †
⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	imcomm-P3.27 265	Commutation of Antecedents. †
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (𝜓 → (𝜑 → 𝜒)))
Theorem	imcomm-P3.27.RC 266	Inference Form of imcomm-P3.27 265. †
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))
Theorem	imsubl-P3.28a 267	Implication Substitution (left). †
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	imsubl-P3.28a.RC 268	Inference Form of imsubl-P3.28a 267. †
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))
Theorem	imsubr-P3.28b 269	Implication Substitution (right). †
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	imsubr-P3.28b.RC 270	Inference Form of imsubr-P3.28b 269. †
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))
Theorem	imsubd-P3.28c 271	Implication Substitution (dual) †. This can also be called "Linking Syllogism" because the result is the statement that adding the missing inner link between the two hypotheses links the entire chain as a consequence. The mneumonic is as follows... If ( 1 → 2 ) and ( 3 → 4 ) then ( ( 2 → 3 ) → ( 1 → 4 ) )... or ( left-middle → right-middle ) → ( left-outer → right-outer ). One can substitute ( 1 → 1 ) for ( 1 → 2 ), or ( 3 → 3 ) for ( 3 → 4 ) to see how imsubr-P3.28b 269 and imsubl-P3.28a 267 are related as special cases.
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜒 → 𝜗))    ⇒   ⊢ (𝛾 → ((𝜓 → 𝜒) → (𝜑 → 𝜗)))
Theorem	imsubd-P3.28c.RC 272	Inference Form of imsubd-P3.28c 271. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜗)    ⇒   ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜗))
4.3.3  Double Negation Laws.
Theorem	dnegi-P3.29 273	Double Negation Introduction. † This statement does not require ndexclmid-P3.16 181, and is thus deducible with intuitionist logic.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ¬ ¬ 𝜑)
Theorem	dnegi-P3.29.RC 274	Inference Form of dnegi-P3.29 273. †
⊢ 𝜑    ⇒   ⊢ ¬ ¬ 𝜑
Theorem	dnegi-P3.29.CL 275	Closed Form of dnegi-P3.29 273. †
⊢ (𝜑 → ¬ ¬ 𝜑)
Theorem	dnege-P3.30 276	Double Negation Elimination. This statement is equivalent to ndexclmid-P3.16 181, thus it is not deducible with intuitionist logic.
⊢ (𝛾 → ¬ ¬ 𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	dnege-P3.30.RC 277	Inference Form of dnege-P3.30 276.
⊢ ¬ ¬ 𝜑    ⇒   ⊢ 𝜑
Theorem	dnege-P3.30.CL 278	Closed Form of dnege-P3.30 276.
⊢ (¬ ¬ 𝜑 → 𝜑)
4.3.4  Transposition Laws (including Axiom L3).
Theorem	trnsp-P3.31a 279	Transposition Variant A (negation introduction). † This statement is the deductive form of trnsp-P1.15a 76. It does not require the Law of Excluded Middle, and is thus deducible with intuitionist logic.
⊢ (𝛾 → (𝜑 → ¬ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → ¬ 𝜑))
Theorem	trnsp-P3.31a.RC 280	Inference Form of trnsp-P3.31a 279. †
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → ¬ 𝜑)
Theorem	trnsp-P3.31a.CL 281	Closed Form of trnsp-P3.31a 279. †
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
Theorem	trnsp-P3.31b 282	Transposition Variant B (negation elimination). This statement is the deductive form of trnsp-P1.15b 78. It is equivalent to Axiom L3 and requires the Law of Excluded Middle. It is thus not deducible with intuitionist logic.
⊢ (𝛾 → (¬ 𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜓 → 𝜑))
Theorem	trnsp-P3.31b.RC 283	Inference Form of trnsp-P3.31b 282.
⊢ (¬ 𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → 𝜑)
Theorem	trnsp-P3.31b.CL 284	Closed Form of trnsp-P3.31b 282.
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))
Theorem	trnsp-P3.31c 285	Transposition Variant C (negation introduction). † This statement is the deductive form of trnsp-P1.15c 80. It does not require the Law of Excluded Middle, and is thus deducible with intuitionist logic.
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜓 → ¬ 𝜑))
Theorem	trnsp-P3.31c.RC 286	Inference Form of trnsp-P3.31c 285. †
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (¬ 𝜓 → ¬ 𝜑)
Theorem	trnsp-P3.31c.CL 287	Closed Form of trnsp-P3.31c 285. †
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Theorem	trnsp-P3.31d 288	Transposition Variant D (negation elimination). This statement is the deductive form of trnsp-P1.15d 83 (and Axiom L3). It requires the Law of Excluded Middle and is thus not deducible with intuitionist logic.
⊢ (𝛾 → (¬ 𝜑 → ¬ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜑))
Theorem	trnsp-P3.31d.RC 289	Inference Form of trnsp-P3.31d 288.
⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	trnsp-P3.31d.CL 290	Closed Form of trnsp-P3.31d 288 (Axiom L3). This is a restatement of Axiom L3, deduced via natural deduction.
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
4.3.5  Other Laws Involving Negation.
Theorem	mt-P3.32a 291	Modus Tollens. † This statement is the deductive form of nclav-P1.14 73. It does not rely on the Law of Excluded Middle, and is thus deducible with intuitionist logic.
⊢ (𝛾 → (𝜑 → ¬ 𝜑))    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	mt-P3.32a.RC 292	Inference Form of mt-P3.32a 291. †
⊢ (𝜑 → ¬ 𝜑)    ⇒   ⊢ ¬ 𝜑
Theorem	mt-3.32a.CL 293	Closed Form of mt-P3.32a 291. †
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
Theorem	nmt-P3.32b 294	Negated Modus Tollens. This statement is the deductive form of clav-P1.12 68. It requires the Law of Excluded Middle and is thus not deducible with intuitionist logic.
⊢ (𝛾 → (¬ 𝜑 → 𝜑))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	nmt-P3.32b.RC 295	Inference Form of nmt-P3.32b 294.
⊢ (¬ 𝜑 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	nmt-3.32b.CL 296	Closed Form of nmt-P3.32b 294.
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
4.4  Revisiting Chapter 2.
4.4.1  Biconditional Equivalence Properties.
Theorem	biref-P3.33a 297	Equivalence Property: '↔' Reflexivity. †
⊢ (𝜑 ↔ 𝜑)
Theorem	bisym-P3.33b 298	Equivalence Property: '↔' Symmetry. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ↔ 𝜑))
Theorem	bisym-P3.33b.RC 299	Inference Form of bisym-P3.33b 298. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ↔ 𝜑)
Theorem	bisym-P3.33b.CL 300	Closed Form of bisym-P3.33b 298. †
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))