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  1692  necon1abid  2668  necon4abid  2671  necon2abid  2674  necon2bbid  2676  necon1abii  2682  nnelOLD  2767  dfral2  2869  ralnex2  2928  ralnex3  2929  elsymdifxor  3699  difsnpss  4143  xpimasn  5301  zfregs2  8226  nqereu  9362  ssnn0fi  12204  ncoprmlnprm  14677  cusgrares  25199  uvtx01vtx  25219  wlkcpr  25256  vdn0frgrav2  25750  vdgn0frgrav2  25751  xrdifh  28369  ballotlemfc0  29334  ballotlemfcc  29335  bnj1143  29611  bnj1304  29640  bnj1189  29827  bj-nfn  31219  wl-nfnbi  31824  tsim1  32337  tsna1  32351  ifpxorcor  36091  ifpnot23b  36097  ifpnot23c  36099  ifpnot23d  36100  iunrelexp0  36265  dfss6  36334  con5VD  37271  sineq0ALT  37308  jcn  37342  nepnfltpnf  37520  nemnftgtmnft  37522  sge0gtfsumgt  38194  nnfoctbdjlem  38202  iatbtatnnb  38371  atbiffatnnb  38372  falseral0  38855  lindslinindsimp2  39907  islininds2  39928  nnolog2flm1  40052
  Copyright terms: Public domain W3C validator