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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imnan | |
|
2 | pm4.62 | |
|
3 | 1 2 | bitr3i | |