![]() |
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 870 | . 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
2 | 3orass 1089 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | df-3or 1087 | . 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∨ wo 847 ∨ w3o 1085 |
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-or 848 df-3or 1087 |
This theorem is referenced by: 3orcomb 1093 3mix2 1330 3mix3 1331 3orel2 1483 eueq3 3719 tprot 4753 wemapsolem 9587 ssxr 11327 elnnz 12620 elznn 12626 pfxnd0 14722 nolt02o 27754 nosupbnd2lem1 27774 colrot1 28581 lnrot1 28645 lnrot2 28646 dfon2lem5 35768 dfon2lem6 35769 colinearperm3 36044 wl-exeq 37514 dvasin 37690 frege129d 43752 usgrexmpl2nb0 47925 usgrexmpl2nb3 47928 |
Copyright terms: Public domain | W3C validator |