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  1954  zfregs2  7299  konigthlem  8070  nqereu  8433  sqrmo  11614  boxeq  24152  albineal  24164  deref  24454  iatbtatnnb  26962  atbiffatnnb  26963  con5VD  27463  bnj1143  27608  bnj1304  27638  bnj1189  27825  bnj1204  27828  a12studyALT  28037
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