Theorem ioran 304

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		notnot 159	. . . 4 |- (ph <-> -. -. ph)
2		notnot 159	. . . 4 |- (ps <-> -. -. ps)
3	1, 2	orbi12i 255	. . 3 |- ((ph \/ ps) <-> (-. -. ph \/ -. -. ps))
4	3	notbii 185	. 2 |- (-. (ph \/ ps) <-> -. (-. -. ph \/ -. -. ps))
5		anor 302	. 2 |- ((-. ph /\ -. ps) <-> -. (-. -. ph \/ -. -. ps))
6	4, 5	bitr4i 174	1 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Syntax hints:  -. wn 2   <-> wb 144   \/ wo 220   /\ wa 221

This theorem is referenced by:  pm4.56 309  oran 310  pm3.2ni 583  andi 607  dfbi3 673  xor2 676  ecase2d 756  ecase3 757  dn1 779  3ori 891  ecase23d 929  19.43 1124  equvini 1205  dfun2 2295  sspr 2540  sotrieq 2940  sotrieq2 2941  wereu 2972  ordtri3 3011  ordtri4 3012  ordnbtwn 3062  dfwe2 3140  dflim3 3201  dfrdg2 4234  oalimcl 4330  omlimcl 4345  1re 5589  ltxrlt 5654  elnnz 6313  elnnz1 6323  om2uzf1oi 6664  sqrlem13 6886  elcncf 7470  nonbooli 9874  cvnbtwn4 10497  irredi 10603  atcvat4i 10606  ordtypelem6 11432  extbas1 11641  ufileu 11658

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 145  df-or 222  df-an 223

Copyright terms: Public domain