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

Theorem notnot1 116
Description: Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Assertion
Ref Expression
notnot1  |-  ( ph  ->  -.  -.  ph )

Proof of Theorem notnot1
StepHypRef Expression
1 id 20 . 2  |-  ( -. 
ph  ->  -.  ph )
21con2i 114 1  |-  ( ph  ->  -.  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  notnoti  117  con1d  118  con4i  124  notnot  283  biortn  396  pm2.13  408  eueq2  3108  ifnot  3777  nbusgra  21440  wlkntrl  21562  eupath2  21702  stoweidlem39  27764  vk15.4j  28612  zfregs2VD  28953  vk15.4jVD  29026  con3ALTVD  29028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator