Theorem 3orass 981

Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3orass	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Proof of Theorem 3orass

Step	Hyp	Ref	Expression
1		df-3or 979	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 767	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 184	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

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