This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem anor

Description: Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 3-Nov-2012)

Ref Expression
Assertion anor ⊢ φ ∧ ψ ↔ ¬ ¬ φ ∨ ¬ ψ

Proof

Step Hyp Ref Expression
1 notnotb ⊢ φ ∧ ψ ↔ ¬ ¬ φ ∧ ψ
2 ianor ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∨ ¬ ψ
3 1 2 xchbinx ⊢ φ ∧ ψ ↔ ¬ ¬ φ ∨ ¬ ψ