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

Theorem notnot 284
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 116 . 2  |-  ( ph  ->  -.  -.  ph )
2 notnot2 106 . 2  |-  ( -. 
-.  ph  ->  ph )
31, 2impbii 182 1  |-  ( ph  <->  -. 
-.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178
This theorem is referenced by:  notbid  287  con2bi  320  con1bii  323  imor  403  iman  415  dfbi3  868  alex  1570  sbn  1955  difsnpss  3718  zfregs2  7369  konigthlem  8144  nqereu  8507  ballotlemfc0  22998  ballotlemfcc  22999  ballotlemi1  23008  ballotlemii  23009  boxeq  24339  albineal  24351  deref  24641  aisbnaxb  27154  iatbtatnnb  27155  atbiffatnnb  27156  con5VD  27710  bnj1143  27855  bnj1304  27885  bnj1189  28072  bnj1204  28075  a12studyALT  28284
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator