![]() |
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 869 | . 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
2 | 3orass 1091 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | df-3or 1089 | . 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
4 | 1, 2, 3 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 ∨ w3o 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-or 847 df-3or 1089 |
This theorem is referenced by: 3orcomb 1095 3mix2 1332 3mix3 1333 3orel2 1486 eueq3 3708 tprot 4754 wemapsolem 9545 ssxr 11283 elnnz 12568 elznn 12574 pfxnd0 14638 nolt02o 27198 nosupbnd2lem1 27218 colrot1 27810 lnrot1 27874 lnrot2 27875 dfon2lem5 34759 dfon2lem6 34760 colinearperm3 35035 wl-exeq 36403 dvasin 36572 frege129d 42514 |
Copyright terms: Public domain | W3C validator |