Theorem pm4.13 161

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

Assertion

Ref	Expression
pm4.13	|- (ph <-> -. -. ph)

Proof of Theorem pm4.13

Step	Hyp	Ref	Expression
1		negb 86	. 2 |- (ph -> -. -. ph)
2		nega 84	. 2 |- (-. -. ph -> ph)
3	1, 2	impbi 157	1 |- (ph <-> -. -. ph)

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

This theorem is referenced by:  imor 234  iman 237  ianor 305  ioran 306  pm4.52 307  pm4.54 309  oran 312  oranabs 580  xor 669  alex 1030  sbn 1226  a12studyALT 1372  symdif2 2256  chrelat2 10200

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 147

Copyright terms: Public domain