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 | |- ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imnan | |- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) ) |
|
| 2 | pm4.62 | |- ( ( ph -> -. ps ) <-> ( -. ph \/ -. ps ) ) |
|
| 3 | 1 2 | bitr3i | |- ( -. ( ph /\ ps ) <-> ( -. ph \/ -. ps ) ) |