Theorem ianor 305

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

Assertion

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

Proof of Theorem ianor

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

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

This theorem is referenced by:  pm4.79 355  andi 603  pm3.24 657  pm5.18 659  pm5.16 666  19.33b 1090  19.41 1093  neorian 1637  pssn2lp 2143  ordtri3or 2974  suc11 3088  xpeq0 3459  imadif 3566  mapdom2 4480  suc11reg 4585  rankxplim3 4694  kmlem3 4747  ssgt0sr 5197  xrrebndt 5549  bcval4t 6907  efif1lem5 8668  chrelat2 10229  atcvat 10250  cdrci 10417

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