|   | 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.) Shorten with xchnxbir 333. (Revised by Wolf Lammen, 8-Apr-2022.) | 
| Ref | Expression | 
|---|---|
| 3ianor | ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ianor 983 | . . 3 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
| 2 | 1 | orbi1i 913 | . 2 ⊢ ((¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | 
| 3 | ianor 983 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | |
| 4 | df-3an 1088 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
| 5 | 3, 4 | xchnxbir 333 | . 2 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ (𝜑 ∧ 𝜓) ∨ ¬ 𝜒)) | 
| 6 | df-3or 1087 | . 2 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ 𝜒)) | |
| 7 | 2, 5, 6 | 3bitr4i 303 | 1 ⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 | 
| 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 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 | 
| This theorem is referenced by: 3anor 1107 tppreqb 4804 otthne 5490 fr3nr 7793 bropopvvv 8116 prinfzo0 13739 elfznelfzo 13812 ssnn0fi 14027 hashtpg 14525 hash3tpde 14533 swrdnd0 14696 pfxnd0 14727 lcmfunsnlem2lem2 16677 prm23ge5 16854 2irrexpq 26774 lpni 30500 xrdifh 32783 dvasin 37712 dflim5 43347 limcicciooub 45657 2zrngnring 48179 | 
| Copyright terms: Public domain | W3C validator |