![]() |
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 980 | . . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
2 | 1 | orbi1i 912 | . 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) |
3 | ianor 980 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | |
4 | df-3an 1089 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
5 | 3, 4 | xchnxbir 332 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) |
6 | df-3or 1088 | . 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | |
7 | 2, 5, 6 | 3bitr4i 302 | 1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∨ w3o 1086 ∧ w3a 1087 |
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 846 df-3or 1088 df-3an 1089 |
This theorem is referenced by: 3anor 1108 tppreqb 4808 otthne 5486 fr3nr 7758 bropopvvv 8075 prinfzo0 13670 elfznelfzo 13736 ssnn0fi 13949 hashtpg 14445 swrdnd0 14606 pfxnd0 14637 lcmfunsnlem2lem2 16575 prm23ge5 16747 2irrexpq 26237 lpni 29728 xrdifh 31986 dvasin 36567 dflim5 42069 limcicciooub 44343 2zrngnring 46840 |
Copyright terms: Public domain | W3C validator |