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  8547  nbssntrs  26250  conimpf  27989  con3ALT  28592  zfregs2VD  28933  con3ALTVD  29008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator