Theorem 3orass 1008

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

Syntax hints:   ↔ wb 105   ∨ wo 716   ∨ w3o 1004

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 717

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

This theorem is referenced by:  3orrot  1011  3orcomb  1014  3mix1  1193  3bior1fd  1389  sotritric  4450  sotritrieq  4451  ordtriexmid  4648  ontriexmidim  4649  acexmidlemcase  6053  nntri3or  6739  nntri2  6740  exmidontriimlem1  7541  elnnz  9604  elznn0  9609  elznn  9610  zapne  9669  nn01to3  9967  elxr  10128  bezoutlemmain  12719  nninfctlemfo  12761  lgsdilem  16026  gausslemma2dlem4  16063