Theorem negb 86

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 84	. 2 |- (-. -. -. ph -> -. ph)
2	1	a3i 74	1 |- (ph -> -. -. ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  negbi 87  con1 92  con3 94  con1i 96  pm4.13 161  pm2.13 655  eueq2 1909  eueq3 1910  ifswap 2372

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

Copyright terms: Public domain