Theorem nega 84

Description: Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (The proof was shortened by David Harvey, 5-Sep-99. An even shorter proof found by Josh Purinton, 29-Dec-00.)

Assertion

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

Proof of Theorem nega

Step	Hyp	Ref	Expression
1		pm2.21 76	. 2 |- (-. -. ph -> (-. ph -> ph))
2		pm2.18 81	. 2 |- ((-. ph -> ph) -> ph)
3	1, 2	syl 10	1 |- (-. -. ph -> ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  negai 85  negb 86  pm2.01 88  con2 90  con2i 97  con3i 98  pm4.13 161  condan 477  pm2.1 654  pm2.26 657  indpi 5006

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

Copyright terms: Public domain