Theorem 3orass 1007

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

Syntax hints:   ↔ wb 105   ∨ wo 715   ∨ w3o 1003

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 716

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

This theorem is referenced by:  3orrot  1010  3orcomb  1013  3mix1  1192  3bior1fd  1388  sotritric  4421  sotritrieq  4422  ordtriexmid  4619  ontriexmidim  4620  acexmidlemcase  6012  nntri3or  6660  nntri2  6661  exmidontriimlem1  7435  elnnz  9488  elznn0  9493  elznn  9494  zapne  9553  nn01to3  9850  elxr  10010  bezoutlemmain  12568  nninfctlemfo  12610  lgsdilem  15755  gausslemma2dlem4  15792