Theorem notnot 291

Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.)

Assertion

Ref	Expression
notnot

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		notnot1 122	. 2
2		notnot2 112	. 2
3	1, 2	impbii 188	1

Syntax hints:  -.wn 3  <->wb 184

This theorem is referenced by:  notbid  294  con2bi  328  con1bii  331  imor  412  iman  424  dfbi3  893  ifpn  1391  alex  1647  necon1abid  2705  necon4abid  2708  necon2abid  2711  necon2bbid  2713  necon1abii  2719  nnelOLD  2803  dfral2  2904  difsnpss  4173  xpimasn  5457  zfregs2  8185  nqereu  9328  ssnn0fi  12094  cusgrares  24472  uvtx01vtx  24492  wlkcpr  24529  vdn0frgrav2  25023  vdgn0frgrav2  25024  xrdifh  27591  ballotlemfc0  28431  ballotlemfcc  28432  wl-nfnbi  29979  tsim1  30537  tsna1  30551  jcn  31427  ralnex2  31435  iatbtatnnb  32107  atbiffatnnb  32108  lindslinindsimp2  33064  islininds2  33085  elsymdifxor  33217  con5VD  33700  sineq0ALT  33737  bnj1143  33849  bnj1304  33878  bnj1189  34065  bj-nfn  34219  bj-ifororb  37726  dfss6  37792

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