MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notnot2 Unicode version

Theorem notnot2 106
Description: Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (Contributed by NM, 5-Aug-1993.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Assertion
Ref Expression
notnot2  |-  ( -. 
-.  ph  ->  ph )

Proof of Theorem notnot2
StepHypRef Expression
1 pm2.21 102 . 2  |-  ( -. 
-.  ph  ->  ( -. 
ph  ->  ph ) )
21pm2.18d 105 1  |-  ( -. 
-.  ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  notnotrd  107  notnotri  108  con2d  109  con3d  127  notnot  284  condan  771  ecase3ad  913  indpi  8526  nbssntrs  25546  conimpf  27265  con3ALT  27564  zfregs2VD  27885  con3ALTVD  27960
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator