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  891  alex  1627  sbnOLD  2106  necon1abid  2715  necon4abid  2718  necon2abid  2721  necon2bbid  2723  necon1abii  2729  nnelOLD  2813  dfral2  2911  difsnpss  4170  xpimasn  5450  zfregs2  8160  nqereu  9303  ssnn0fi  12058  cusgrares  24148  uvtx01vtx  24168  wlkcpr  24205  vdn0frgrav2  24700  vdgn0frgrav2  24701  xrdifh  27259  ballotlemfc0  28071  ballotlemfcc  28072  wl-nfnbi  29556  tsim1  30141  tsna1  30155  jcn  31009  ralnex2  31017  iatbtatnnb  31574  atbiffatnnb  31575  lindslinindsimp2  32137  islininds2  32158  con5VD  32780  sineq0ALT  32817  bnj1143  32928  bnj1304  32957  bnj1189  33144  bj-ifn  33236  bj-nfn  33307
  Copyright terms: Public domain W3C validator