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 963 | . 2 | |
2 | orass 756 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 697 w3o 961 |
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 698 |
This theorem depends on definitions: df-bi 116 df-3or 963 |
This theorem is referenced by: 3orrot 968 3orcomb 971 3mix1 1150 sotritric 4241 sotritrieq 4242 ordtriexmid 4432 acexmidlemcase 5762 nntri3or 6382 nntri2 6383 elnnz 9057 elznn0 9062 elznn 9063 zapne 9118 nn01to3 9402 elxr 9556 bezoutlemmain 11675 |
Copyright terms: Public domain | W3C validator |