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

Theorem notnot 291
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 122 . 2  |-  ( ph  ->  -.  -.  ph )
2 notnot2 112 . 2  |-  ( -. 
-.  ph  ->  ph )
31, 2impbii 188 1  |-  ( ph  <->  -. 
-.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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 185
This theorem is referenced by:  notbid  294  con2bi  328  con1bii  331  imor  412  iman  424  dfbi3  893  alex  1634  necon1abid  2691  necon4abid  2694  necon2abid  2697  necon2bbid  2699  necon1abii  2705  nnelOLD  2789  dfral2  2890  difsnpss  4158  xpimasn  5442  zfregs2  8167  nqereu  9310  ssnn0fi  12073  cusgrares  24344  uvtx01vtx  24364  wlkcpr  24401  vdn0frgrav2  24895  vdgn0frgrav2  24896  xrdifh  27463  ballotlemfc0  28304  ballotlemfcc  28305  wl-nfnbi  29954  tsim1  30512  tsna1  30526  jcn  31381  ralnex2  31389  iatbtatnnb  31945  atbiffatnnb  31946  lindslinindsimp2  32799  islininds2  32820  con5VD  33433  sineq0ALT  33470  bnj1143  33582  bnj1304  33611  bnj1189  33798  bj-ifn  33903  bj-nfn  33967
  Copyright terms: Public domain W3C validator