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

Theorem notnot 289
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  292  con2bi  326  con1bii  329  imor  410  iman  422  dfbi3  891  ifpn  1390  alex  1652  necon1abid  2702  necon4abid  2705  necon2abid  2708  necon2bbid  2710  necon1abii  2716  nnelOLD  2800  dfral2  2901  elsymdifxor  3721  difsnpss  4159  xpimasn  5437  zfregs2  8155  nqereu  9296  ssnn0fi  12076  cusgrares  24674  uvtx01vtx  24694  wlkcpr  24731  vdn0frgrav2  25225  vdgn0frgrav2  25226  xrdifh  27825  ballotlemfc0  28695  ballotlemfcc  28696  wl-nfnbi  30219  tsim1  30777  tsna1  30791  jcn  31667  ralnex2  31675  iatbtatnnb  32346  atbiffatnnb  32347  lindslinindsimp2  33318  islininds2  33339  nnolog2flm1  33465  con5VD  34101  sineq0ALT  34138  bnj1143  34250  bnj1304  34279  bnj1189  34466  bj-nfn  34620  ifpnot23b  38120  ifpnot23c  38121  ifpnot23d  38122  ifpororb  38133  ifpxorcor  38144  iunrelexp0  38224  dfss6  38242
  Copyright terms: Public domain W3C validator