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  865  alex  1560  19.8w  1660  sbn  2001  difsnpss  3759  zfregs2  7410  konigthlem  8185  nqereu  8548  ballotlemfc0  23044  ballotlemfcc  23045  ballotlemi1  23054  ballotlemii  23055  boxeq  24385  albineal  24397  deref  24687  aisbnaxb  27258  iatbtatnnb  27259  atbiffatnnb  27260  con5VD  27944  bnj1143  28089  bnj1304  28119  bnj1189  28306  bnj1204  28309  a12studyALT  28400
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