Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-cases2-dnf | Structured version Visualization version GIF version |
Description: A particular instance of orddi 1007 and anddi 1008 converting between disjunctive and conjunctive normal forms, when both 𝜑 and ¬ 𝜑 appear. This theorem in fact rephrases cases2 1045, and is related to consensus 1050. I restate it here in DNF and CNF. The proof deliberately does not use df-ifp 1061 and dfifp4 1064, by which it can be shortened. (Contributed by Wolf Lammen, 21-Jun-2020.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
wl-cases2-dnf | ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmid 892 | . . . . 5 ⊢ (𝜑 ∨ ¬ 𝜑) | |
2 | 1 | biantrur 531 | . . . 4 ⊢ ((𝜑 ∨ 𝜒) ↔ ((𝜑 ∨ ¬ 𝜑) ∧ (𝜑 ∨ 𝜒))) |
3 | orcom 867 | . . . . 5 ⊢ ((¬ 𝜑 ∨ 𝜓) ↔ (𝜓 ∨ ¬ 𝜑)) | |
4 | orcom 867 | . . . . 5 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒)) | |
5 | 3, 4 | anbi12i 627 | . . . 4 ⊢ (((¬ 𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜓)) ↔ ((𝜓 ∨ ¬ 𝜑) ∧ (𝜓 ∨ 𝜒))) |
6 | 2, 5 | anbi12i 627 | . . 3 ⊢ (((𝜑 ∨ 𝜒) ∧ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜓))) ↔ (((𝜑 ∨ ¬ 𝜑) ∧ (𝜑 ∨ 𝜒)) ∧ ((𝜓 ∨ ¬ 𝜑) ∧ (𝜓 ∨ 𝜒)))) |
7 | anass 469 | . . 3 ⊢ ((((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) ∧ (𝜒 ∨ 𝜓)) ↔ ((𝜑 ∨ 𝜒) ∧ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜓)))) | |
8 | orddi 1007 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ (((𝜑 ∨ ¬ 𝜑) ∧ (𝜑 ∨ 𝜒)) ∧ ((𝜓 ∨ ¬ 𝜑) ∧ (𝜓 ∨ 𝜒)))) | |
9 | 6, 7, 8 | 3bitr4ri 304 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ (((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) ∧ (𝜒 ∨ 𝜓))) |
10 | wl-orel12 35670 | . . 3 ⊢ (((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) → (𝜒 ∨ 𝜓)) | |
11 | 10 | pm4.71i 560 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) ↔ (((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) ∧ (𝜒 ∨ 𝜓))) |
12 | ancom 461 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∧ (¬ 𝜑 ∨ 𝜓)) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) | |
13 | 9, 11, 12 | 3bitr2i 299 | 1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 396 ∨ wo 844 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |