![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ianor | Structured version Visualization version GIF version |
Description: Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Revised by Wolf Lammen, 8-Apr-2022.) |
Ref | Expression |
---|---|
3ianor | ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ianor 981 | . . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
2 | 1 | orbi1i 913 | . 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) |
3 | ianor 981 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | |
4 | df-3an 1090 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
5 | 3, 4 | xchnxbir 333 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) |
6 | df-3or 1089 | . 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | |
7 | 2, 5, 6 | 3bitr4i 303 | 1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∨ w3o 1087 ∧ w3a 1088 |
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 398 df-or 847 df-3or 1089 df-3an 1090 |
This theorem is referenced by: 3anor 1109 tppreqb 4769 otthne 5447 fr3nr 7710 bropopvvv 8026 prinfzo0 13620 elfznelfzo 13686 ssnn0fi 13899 hashtpg 14393 swrdnd0 14554 pfxnd0 14585 lcmfunsnlem2lem2 16523 prm23ge5 16695 2irrexpq 26108 lpni 29471 xrdifh 31737 dvasin 36212 dflim5 41711 limcicciooub 43968 2zrngnring 46340 |
Copyright terms: Public domain | W3C validator |