Theorem negb 79

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

Assertion

Ref	Expression
negb	|- (ph -> -. -. ph)

Proof of Theorem negb

Step	Hyp	Ref	Expression
1		nega 78	. 2 |- (-. -. -. ph -> -. ph)
2	1	a3i 69	1 |- (ph -> -. -. ph)

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