Theorem negb 79

Description: Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101.

Assertion

Ref	Expression
negb	⊢ (φ → ¬ ¬ φ)

Proof of Theorem negb

Step	Hyp	Ref	Expression
1		nega 78	. 2 ⊢ (¬ ¬ ¬ φ → ¬ φ)
2	1	a3i 69	1 ⊢ (φ → ¬ ¬ φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  con1 84  con3 86  con1i 88  pm4.13 142  eueq2 1429  eueq3 1430  dm0 2542  dmsn0 2543  dmsnsn0 2544  abianfp 3000

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org