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 580  andi 604  dfbi3 670  xor2 673  ecase2d 751  ecase3 752  3ori 885  ecase23d 922  19.43 1088  equvini 1168  dfun2 2243  sspr 2475  sotrieq 2861  sotrieq2 2862  dfwe2 2935  wereu 2945  ordtri3 2983  ordtri4 2984  ordnbtwn 3063  dflim3 3118  dfrdg2 3933  oalimcl 4194  omlimcl 4209  1re 5435  ltxrltt 5500  elnnz 6145  elnnz1 6155  om2uzf1o 6301  sqrlem13 6685  elcncf 7265  nonbool 9596  cvnbtwn4t 10216  irred 10321  atcvat4 10324

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