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 ¬φψ¬φ¬ψ