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 968 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
2 | orass 757 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | bitri 183 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 698 ∨ w3o 966 |
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 699 |
This theorem depends on definitions: df-bi 116 df-3or 968 |
This theorem is referenced by: 3orrot 973 3orcomb 976 3mix1 1155 sotritric 4296 sotritrieq 4297 ordtriexmid 4492 ontriexmidim 4493 acexmidlemcase 5831 nntri3or 6452 nntri2 6453 exmidontriimlem1 7168 elnnz 9192 elznn0 9197 elznn 9198 zapne 9256 nn01to3 9546 elxr 9703 bezoutlemmain 11916 |
Copyright terms: Public domain | W3C validator |