![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ioran | Structured version Visualization version GIF version |
Description: Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.) |
Ref | Expression |
---|---|
3ioran | ⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioran 985 | . . 3 ⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | |
2 | 1 | anbi1i 624 | . 2 ⊢ ((¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) ∧ ¬ 𝜒)) |
3 | ioran 985 | . . 3 ⊢ (¬ ((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒)) | |
4 | df-3or 1087 | . . 3 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
5 | 3, 4 | xchnxbir 333 | . 2 ⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ (𝜑 ∨ 𝜓) ∧ ¬ 𝜒)) |
6 | df-3an 1088 | . 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: 3oran 1108 cadnot 1612 lcmftp 16670 prm23ge5 16849 cnfldfun 21396 cnfldfunOLD 21409 fbunfip 23893 frgrregord013 30424 wl-nfeqfb 37517 sn-inelr 42474 usgrexmpl2trifr 47932 gpg5nbgrvtx03starlem1 47959 gpg5nbgrvtx03starlem2 47960 gpg5nbgrvtx03starlem3 47961 gpg5nbgrvtx13starlem1 47962 gpg5nbgrvtx13starlem2 47963 gpg5nbgrvtx13starlem3 47964 |
Copyright terms: Public domain | W3C validator |