![]() |
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 979 | . . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
2 | 1 | orbi1i 911 | . 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) |
3 | ianor 979 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | |
4 | df-3an 1086 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
5 | 3, 4 | xchnxbir 332 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) |
6 | df-3or 1085 | . 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | |
7 | 2, 5, 6 | 3bitr4i 302 | 1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 ∨ wo 845 ∨ w3o 1083 ∧ w3a 1084 |
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 395 df-or 846 df-3or 1085 df-3an 1086 |
This theorem is referenced by: 3anor 1105 tppreqb 4813 otthne 5492 fr3nr 7780 bropopvvv 8101 prinfzo0 13711 elfznelfzo 13777 ssnn0fi 13990 hashtpg 14486 swrdnd0 14647 pfxnd0 14678 lcmfunsnlem2lem2 16617 prm23ge5 16791 2irrexpq 26685 lpni 30310 xrdifh 32569 dvasin 37210 dflim5 42789 limcicciooub 45054 2zrngnring 47398 |
Copyright terms: Public domain | W3C validator |