Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3orass | Unicode version |
Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3orass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3or 948 | . 2 | |
2 | orass 741 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 682 w3o 946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 |
This theorem depends on definitions: df-bi 116 df-3or 948 |
This theorem is referenced by: 3orrot 953 3orcomb 956 3mix1 1135 sotritric 4216 sotritrieq 4217 ordtriexmid 4407 acexmidlemcase 5737 nntri3or 6357 nntri2 6358 elnnz 9022 elznn0 9027 elznn 9028 zapne 9083 nn01to3 9365 elxr 9518 bezoutlemmain 11598 |
Copyright terms: Public domain | W3C validator |