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

Theorem notnot 292
Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)
Assertion
Ref Expression
notnot  |-  ( ph  <->  -. 
-.  ph )

Proof of Theorem notnot
StepHypRef Expression
1 notnot1 125 . 2  |-  ( ph  ->  -.  -.  ph )
2 notnot2 115 . 2  |-  ( -. 
-.  ph  ->  ph )
31, 2impbii 190 1  |-  ( ph  <->  -. 
-.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  notbid  295  con2bi  329  con1bii  332  imor  413  iman  425  dfbi3  901  ifpn  1430  alex  1694  necon1abid  2679  necon4abid  2682  necon2abid  2685  necon2bbid  2687  necon1abii  2693  nnelOLD  2778  dfral2  2879  ralnex2  2938  ralnex3  2939  elsymdifxor  3705  difsnpss  4146  xpimasn  5302  zfregs2  8216  nqereu  9353  ssnn0fi  12194  ncoprmlnprm  14648  cusgrares  25045  uvtx01vtx  25065  wlkcpr  25102  vdn0frgrav2  25596  vdgn0frgrav2  25597  xrdifh  28198  ballotlemfc0  29151  ballotlemfcc  29152  bnj1143  29390  bnj1304  29419  bnj1189  29606  bj-nfn  30998  wl-nfnbi  31566  tsim1  32076  tsna1  32090  ifpxorcor  35819  ifpnot23b  35825  ifpnot23c  35827  ifpnot23d  35828  iunrelexp0  35933  dfss6  36000  con5VD  36937  sineq0ALT  36974  jcn  37008  nnfoctbdjlem  37802  iatbtatnnb  37899  atbiffatnnb  37900  lindslinindsimp2  39025  islininds2  39046  nnolog2flm1  39171
  Copyright terms: Public domain W3C validator