| 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 871 | . 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
| 2 | 3orass 1090 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
| 3 | df-3or 1088 | . 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑)) | |
| 4 | 1, 2, 3 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∨ wo 848 ∨ w3o 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-or 849 df-3or 1088 |
| This theorem is referenced by: 3orcomb 1094 3mix2 1332 3mix3 1333 3orel2OLD 1487 eueq3 3717 tprot 4749 wemapsolem 9590 ssxr 11330 elnnz 12623 elznn 12629 pfxnd0 14726 nolt02o 27740 nosupbnd2lem1 27760 colrot1 28567 lnrot1 28631 lnrot2 28632 dfon2lem5 35788 dfon2lem6 35789 colinearperm3 36064 wl-exeq 37535 dvasin 37711 frege129d 43776 usgrexmpl2nb0 47990 usgrexmpl2nb3 47993 |
| Copyright terms: Public domain | W3C validator |