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  1559  19.8w  1659  sbn  2002  difsnpss  3758  zfregs2  7415  konigthlem  8190  nqereu  8553  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemi1  23061  ballotlemii  23062  xrdifh  23273  boxeq  24987  albineal  24999  deref  25288  aisbnaxb  27879  iatbtatnnb  27880  atbiffatnnb  27881  mpt2xopynvov0g  28080  nbusgra  28143  nbgranself2  28151  uvtx01vtx  28164  con5VD  28676  bnj1143  28822  bnj1304  28852  bnj1189  29039  bnj1204  29042  a12studyALT  29133
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