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

Theorem notnot 283
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 181 1  |-  ( ph  <->  -. 
-.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  notbid  286  con2bi  319  con1bii  322  imor  402  iman  414  dfbi3  864  alex  1578  19.8wOLD  1701  sbn  2111  nnel  2665  difsnpss  3901  zfregs2  7625  nqereu  8762  cusgrares  21434  uvtx01vtx  21454  xrdifh  24096  ballotlemfc0  24703  ballotlemfcc  24704  iatbtatnnb  27747  atbiffatnnb  27748  vdn0frgrav2  28128  vdgn0frgrav2  28129  con5VD  28721  bnj1143  28867  bnj1304  28897  bnj1189  29084  sbnNEW7  29266
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 178
  Copyright terms: Public domain W3C validator