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 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 105   ∨ wo 720   ∨ w3o 1008

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 721

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

This theorem is referenced by:  3orrot  1015  3orcomb  1018  3mix1  1197  3bior1fd  1393  sotritric  4464  sotritrieq  4465  ordtriexmid  4663  ontriexmidim  4664  acexmidlemcase  6070  nntri3or  6756  nntri2  6757  exmidontriimlem1  7567  elnnz  9633  elznn0  9638  elznn  9639  zapne  9698  nn01to3  9996  elxr  10157  bezoutlemmain  12753  nninfctlemfo  12795  lgsdilem  16060  gausslemma2dlem4  16097