![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3orass | GIF 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: ↔ wb 105 ∨ wo 708 ∨ w3o 977 |
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 4326 sotritrieq 4327 ordtriexmid 4522 ontriexmidim 4523 acexmidlemcase 5872 nntri3or 6496 nntri2 6497 exmidontriimlem1 7222 elnnz 9265 elznn0 9270 elznn 9271 zapne 9329 nn01to3 9619 elxr 9778 bezoutlemmain 12001 lgsdilem 14513 |
Copyright terms: Public domain | W3C validator |