![]() |
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 979 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | orass 767 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitri 184 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions: df-bi 117 df-3or 979 |
This theorem is referenced by: 3orrot 984 3orcomb 987 3mix1 1166 sotritric 4324 sotritrieq 4325 ordtriexmid 4520 ontriexmidim 4521 acexmidlemcase 5869 nntri3or 6493 nntri2 6494 exmidontriimlem1 7219 elnnz 9261 elznn0 9266 elznn 9267 zapne 9325 nn01to3 9615 elxr 9774 bezoutlemmain 11993 lgsdilem 14321 |
Copyright terms: Public domain | W3C validator |