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

Metamath Proof Explorer

Theorem ianor

Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of WhiteheadRussell p. 120. (Contributed by NM, 14-May-1993) (Proof shortened by Andrew Salmon, 13-May-2011)

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

Proof

Step Hyp Ref Expression
1 imnan ⊢ φ → ¬ ψ ↔ ¬ φ ∧ ψ
2 pm4.62 ⊢ φ → ¬ ψ ↔ ¬ φ ∨ ¬ ψ
3 1 2 bitr3i ⊢ ¬ φ ∧ ψ ↔ ¬ φ ∨ ¬ ψ