Theorem ioran 254

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 142	. . . 4 |- (ph <-> -. -. ph)
2		pm4.13 142	. . . 4 |- (ps <-> -. -. ps)
3	1, 2	orbi12i 216	. . 3 |- ((ph \/ ps) <-> (-. -. ph \/ -. -. ps))
4	3	negbii 162	. 2 |- (-. (ph \/ ps) <-> -. (-. -. ph \/ -. -. ps))
5		anor 252	. 2 |- ((-. ph /\ -. ps) <-> -. (-. -. ph \/ -. -. ps))
6	4, 5	bitr4 154	1 |- (-. (ph \/ ps) <-> (-. ph /\ -. ps))

Syntax hints:  -. wn 1   <-> wb 127   \/ wo 195   /\ wa 196

This theorem is referenced by:  oran 255  pm3.2ni 440  andi 456  dfbi 499  ecase2d 558  ecase3 559  ecased 643  19.43 767  eqvin.l1 851  dfun2 1668  sotrieq 2149  sotrieq2 2150  dfwe2 2187  wereu 2197  ordtri3 2234  ordtri4 2235  ordnbtwn 2316  dflim3 2368  oalimcl 3162  muln0bt 4213  elnnz 4572  elnnz1 4581  om2uzf1o 4656  sqrlem13 4743  cvnbtwn4t 5721  atcvat4 5775

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org