Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3orrot | Structured version Visualization version GIF version |
Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3orrot | ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 401 | . 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
2 | 3orass 1034 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | df-3or 1032 | . 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 291 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∨ wo 382 ∨ w3o 1030 |
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 196 df-or 384 df-3or 1032 |
This theorem is referenced by: 3mix2 1224 3mix3 1225 eueq3 3348 tprot 4228 wemapsolem 8338 ssxr 9986 elnnz 11264 elznn 11270 colrot1 25254 lnrot1 25318 lnrot2 25319 3orel2 30847 dfon2lem5 30936 dfon2lem6 30937 colinearperm3 31340 wl-exeq 32500 dvasin 32666 frege129d 37074 |
Copyright terms: Public domain | W3C validator |