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 978 | . . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
2 | 1 | orbi1i 910 | . 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) |
3 | ianor 978 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | |
4 | df-3an 1085 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
5 | 3, 4 | xchnxbir 335 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) |
6 | df-3or 1084 | . 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | |
7 | 2, 5, 6 | 3bitr4i 305 | 1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∨ w3o 1082 ∧ w3a 1083 |
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 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 |
This theorem is referenced by: 3anor 1104 tppreqb 4731 fr3nr 7488 bropopvvv 7779 prinfzo0 13070 elfznelfzo 13136 ssnn0fi 13347 hashtpg 13837 swrdnd0 14013 pfxnd0 14044 lcmfunsnlem2lem2 15977 prm23ge5 16146 2irrexpq 25307 lpni 28251 xrdifh 30497 dvasin 34972 limcicciooub 41911 2zrngnring 44217 |
Copyright terms: Public domain | W3C validator |