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 867 | . 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 205 ∨ wo 844 ∨ 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 206 df-or 845 df-3or 1087 |
This theorem is referenced by: 3orcomb 1093 3mix2 1330 3mix3 1331 3orel2 1484 eueq3 3646 tprot 4685 wemapsolem 9309 ssxr 11044 elnnz 12329 elznn 12335 pfxnd0 14401 colrot1 26920 lnrot1 26984 lnrot2 26985 dfon2lem5 33763 dfon2lem6 33764 nolt02o 33898 nosupbnd2lem1 33918 colinearperm3 34365 wl-exeq 35693 dvasin 35861 frege129d 41371 |
Copyright terms: Public domain | W3C validator |