Theorem 3orass 1005

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

Syntax hints:   ↔ wb 105   ∨ wo 713   ∨ w3o 1001

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 714

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

This theorem is referenced by:  3orrot  1008  3orcomb  1011  3mix1  1190  3bior1fd  1386  sotritric  4415  sotritrieq  4416  ordtriexmid  4613  ontriexmidim  4614  acexmidlemcase  5996  nntri3or  6639  nntri2  6640  exmidontriimlem1  7403  elnnz  9456  elznn0  9461  elznn  9462  zapne  9521  nn01to3  9812  elxr  9972  bezoutlemmain  12519  nninfctlemfo  12561  lgsdilem  15706  gausslemma2dlem4  15743