![]() |
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 946 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
2 | orass 739 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | bitri 183 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 680 ∨ w3o 944 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 |
This theorem depends on definitions: df-bi 116 df-3or 946 |
This theorem is referenced by: 3orrot 951 3orcomb 954 3mix1 1133 sotritric 4206 sotritrieq 4207 ordtriexmid 4397 acexmidlemcase 5723 nntri3or 6343 nntri2 6344 elnnz 8968 elznn0 8973 elznn 8974 zapne 9029 nn01to3 9311 elxr 9456 bezoutlemmain 11532 |
Copyright terms: Public domain | W3C validator |