Theorem ianor 253

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

Assertion

Ref	Expression
ianor	⊢ (¬ (φ ∧ ψ) ↔ (¬ φ ∨ ¬ ψ))

Proof of Theorem ianor

Step	Hyp	Ref	Expression
1		anor 252	. . 3 ⊢ ((φ ∧ ψ) ↔ ¬ (¬ φ ∨ ¬ ψ))
2	1	negbii 162	. 2 ⊢ (¬ (φ ∧ ψ) ↔ ¬ ¬ (¬ φ ∨ ¬ ψ))
3		pm4.13 142	. 2 ⊢ ((¬ φ ∨ ¬ ψ) ↔ ¬ ¬ (¬ φ ∨ ¬ ψ))
4	2, 3	bitr4 154	1 ⊢ (¬ (φ ∧ ψ) ↔ (¬ φ ∨ ¬ ψ))

Syntax hints:  ¬ wn 1   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  andi 456  pm3.24 496  pm5.18 497  19.33b 771  19.41 774  pssn2lp 1571  prex 1892  ordtri3or 2230  suc11 2341  imadif 2714  mapdom2 3389  suc11reg 3456  kmlem3 3582  kmlem4 3583  ssgt0sr 4011  chrelat2 5758  atcvat 5771

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