Theorem notnot 178

Description: Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
notnot	|- (ph <-> -. -. ph)

Proof of Theorem notnot

Step	Hyp	Ref	Expression
1		notnot1 102	. 2 |- (ph -> -. -. ph)
2		notnot2 100	. 2 |- (-. -. ph -> ph)
3	1, 2	impbii 174	1 |- (ph <-> -. -. ph)

Syntax hints:  -. wn 2   <-> wb 163

This theorem is referenced by:  imor 251  iman 256  ianorOLD 330  ioranOLD 332  pm4.52 333  pm4.54 335  oranOLD 339  oranabs 642  pm5.18 722  xor 734  3ianorOLD 871  alex 1381  sbn 1601  a12studyALT 1770  symdif2OLD 2858  chrelat2i 11937  bnj30OLD 12396  bnj112 12457  bnj1144 12941  bnj1194 12971  bnj1217 12990  bnj1222 12995  bnj1392 13106  bnj1393 13107  bnj1394 13108  bnj1473 13148  boxeq 14314  albineal 14323  deref 14633  alexsublem4 15440  reconnlem1 15446  hlrelat2 17052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain