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

Theorem notnot1 114
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 19 . 2  |-  ( -. 
ph  ->  -.  ph )
21con2i 112 1  |-  ( ph  ->  -.  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  notnoti  115  con1d  116  con4i  122  notnot  282  biortn  395  pm2.13  407  eueq2  2952  ifnot  3616  eupath2  23919  stoweidlem39  27891  atbiffatnnbalt  27986  nbusgra  28277  wlkntrl  28350  vk15.4j  28590  zfregs2VD  28933  vk15.4jVD  29006  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