Theorem 3orass 1012

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

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720   ∨ w3o 1008

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-3or 1010

This theorem is used by:  3orrot  1015  3orcomb  1018  3mix1  1197  3bior1fd  1393  sotritric  4469  sotritrieq  4470  ordtriexmid  4668  ontriexmidim  4669  acexmidlemcase  6080  nntri3or  6766  nntri2  6767  exmidontriimlem1  7577  elnnz  9654  elznn0  9659  elznn  9660  zapne  9719  nn01to3  10017  elxr  10178  bezoutlemmain  12775  nninfctlemfo  12817  lgsdilem  16146  gausslemma2dlem4  16183