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

Theorem notnot2 104
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 100 . 2  |-  ( -. 
-.  ph  ->  ( -. 
ph  ->  ph ) )
21pm2.18d 103 1  |-  ( -. 
-.  ph  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  notnotrd  105  notnotri  106  con2d  107  con3d  125  notnot  282  condan  769  ecase3ad  911  indpi  8531  nbssntrs  26147  conimpf  27886  con3ALT  28293  zfregs2VD  28617  con3ALTVD  28692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator