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

Theorem notnot 282
Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
notnot  |-  ( ph  <->  -. 
-.  ph )

Proof of Theorem notnot
StepHypRef Expression
1 notnot1 114 . 2  |-  ( ph  ->  -.  -.  ph )
2 notnot2 104 . 2  |-  ( -. 
-.  ph  ->  ph )
31, 2impbii 180 1  |-  ( ph  <->  -. 
-.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  notbid  285  con2bi  318  con1bii  321  imor  401  iman  413  dfbi3  863  alex  1572  19.8wOLD  1693  sbn  2067  difsnpss  3837  zfregs2  7505  konigthlem  8280  nqereu  8643  xrdifh  23345  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemi1  24009  ballotlemii  24010  itg2addnclem  25492  aisbnaxb  27202  iatbtatnnb  27203  atbiffatnnb  27204  nnel  27401  mpt2xopynvov0g  27437  nbusgra  27594  nbgranself2  27602  cusgrares  27635  cusgrasizeindslem2  27637  uvtx01vtx  27655  vdn0frgrav2  27857  vdgn0frgrav2  27858  frgrawopreglem4  27880  con5VD  28438  bnj1143  28584  bnj1304  28614  bnj1189  28801  bnj1204  28804  sbnNEW7  28983  a12studyALT  29202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator