Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3orrot | Structured version Visualization version Unicode version |
Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Ref | Expression |
---|---|
3orrot |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom 402 | . 2 | |
2 | 3orass 1040 | . 2 | |
3 | df-3or 1038 | . 2 | |
4 | 1, 2, 3 | 3bitr4i 292 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wo 383 w3o 1036 |
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 197 df-or 385 df-3or 1038 |
This theorem is referenced by: 3mix2 1231 3mix3 1232 eueq3 3381 tprot 4284 wemapsolem 8455 ssxr 10107 elnnz 11387 elznn 11393 colrot1 25454 lnrot1 25518 lnrot2 25519 3orel2 31592 dfon2lem5 31692 dfon2lem6 31693 nolt02o 31845 nosupbnd2lem1 31861 colinearperm3 32170 wl-exeq 33321 dvasin 33496 frege129d 38055 |
Copyright terms: Public domain | W3C validator |