Theorem ioran 306

Description: Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120.

Assertion

Ref	Expression
ioran	|- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Proof of Theorem ioran

Step	Hyp	Ref	Expression
1		pm4.13 161	. . . 4 |- (ph <-> -. -. ph)
2		pm4.13 161	. . . 4 |- (ps <-> -. -. ps)
3	1, 2	orbi12i 257	. . 3 |- ((ph \/ ps) <-> (-. -. ph \/ -. -. ps))
4	3	negbii 187	. 2 |- (-. (ph \/ ps) <-> -. (-. -. ph \/ -. -. ps))
5		anor 304	. 2 |- ((-. ph /\ -. ps) <-> -. (-. -. ph \/ -. -. ps))
6	4, 5	bitr4 176	1 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Syntax hints:  -. wn 2   <-> wb 146   \/ wo 222   /\ wa 223

This theorem is referenced by:  pm4.56 311  oran 312  pm3.2ni 579  andi 603  dfbi 669  xor2 672  ecase2d 750  ecase3 751  3ori 883  ecase23d 920  19.43 1086  equvini 1166  dfun2 2239  sspr 2471  sotrieq 2856  sotrieq2 2857  dfwe2 2930  wereu 2940  ordtri3 2978  ordtri4 2979  ordnbtwn 3058  dflim3 3113  dfrdg2 3924  oalimcl 4184  omlimcl 4199  1re 5415  ltxrltt 5480  elnnz 6100  elnnz1 6110  om2uzf1o 6246  sqrlem13 6623  elcncf 7208  nonbool 9536  cvnbtwn4t 10154  irred 10258  atcvat4 10261

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  df-or 224  df-an 225

Copyright terms: Public domain