Theorem 3orass 984

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 982	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 769	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 184	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 105   ∨ wo 710   ∨ w3o 980

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 711

This theorem depends on definitions:  df-bi 117  df-3or 982

This theorem is referenced by:  3orrot  987  3orcomb  990  3mix1  1169  3bior1fd  1364  sotritric  4371  sotritrieq  4372  ordtriexmid  4569  ontriexmidim  4570  acexmidlemcase  5939  nntri3or  6579  nntri2  6580  exmidontriimlem1  7333  elnnz  9382  elznn0  9387  elznn  9388  zapne  9447  nn01to3  9738  elxr  9898  bezoutlemmain  12319  nninfctlemfo  12361  lgsdilem  15504  gausslemma2dlem4  15541