Theorem 3orass 1089

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 1087	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 921	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 206   ∨ wo 847   ∨ w3o 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-or 848  df-3or 1087

This theorem is referenced by:  3orel1  1090  3orrot  1091  3orcoma  1092  3mix1  1331  ecase23d  1475  3bior1fd  1477  cador  1608  moeq3  3683  sotric  5576  sotrieq  5577  isso2i  5583  ordzsl  7821  soxp  8108  frxp3  8130  wemapsolem  9503  rankxpsuc  9835  tcrank  9837  cardlim  9925  cardaleph  10042  grur1  10773  elnnz  12539  elznn0  12544  elznn  12545  elxr  13076  xrrebnd  13128  xaddf  13184  xrinfmss  13270  elfzlmr  13742  ssnn0fi  13950  hashv01gt1  14310  hashtpg  14450  swrdnd2  14620  pfxnd0  14653  nofv  27569  nosepon  27577  elzs2  28287  elnnzs  28289  elznns  28290  tgldimor  28429  outpasch  28682  xrdifh  32703  eliccioo  32851  orngsqr  33282  elzdif0  33970  qqhval2lem  33971  dfso2  35742  dfon2lem5  35775  dfon2lem6  35776  ecase13d  36301  elicc3  36305  wl-df4-3mintru2  37475  wl-exeq  37522  dvasin  37698  4atlem3a  39591  4atlem3b  39592  frege133d  43754  or3or  44012  3ornot23VD  44836  xrssre  45344  usgrexmpl2nb0  48022  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb5  48027