Theorem ndfalsei-P3.19 184

Description: 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.

Hypothesis

Ref	Expression
ndfalsei-P3.19.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
ndfalsei-P3.19	⊢ (𝜑 → ⊥)

Proof of Theorem ndfalsei-P3.19

Step	Hyp	Ref	Expression
1		ndasm-P3.1 166	. . . 4 ⊢ ((⊤ ∧ 𝜑) → 𝜑)
2		ndfalsei-P3.19.1	. . . . . 6 ⊢ ¬ 𝜑
3	2	ndtruei-P3.17 182	. . . . 5 ⊢ (⊤ → ¬ 𝜑)
4	3	ndimp-P3.2 167	. . . 4 ⊢ ((⊤ ∧ 𝜑) → ¬ 𝜑)
5	1, 4	ndnege-P3.4 169	. . 3 ⊢ ((⊤ ∧ 𝜑) → ⊥)
6	5	ndimi-P3.5 170	. 2 ⊢ (⊤ → (𝜑 → ⊥))
7	6	ndtruee-P3.18 183	1 ⊢ (𝜑 → ⊥)

Syntax hints:  ¬ wff-neg 9   → wff-imp 10   ∧ wff-and 132  ⊤wff-true 153  ⊥wff-false 157

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-true-D2.4 155

This theorem is referenced by:  dffalse-P3.49-L2  364  nthmeqfalse-P4.21b  443