Theorem 3orass 1091

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

Syntax hints:   ↔ wb 205   ∨ wo 846   ∨ w3o 1087

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 206  df-or 847  df-3or 1089

This theorem is referenced by:  3orel1  1092  3orrot  1093  3orcoma  1094  3mix1  1331  ecase23d  1474  3bior1fd  1476  cador  1610  moeq3  3709  sotric  5617  sotrieq  5618  isso2i  5624  ordzsl  7834  soxp  8115  frxp3  8137  wemapsolem  9545  rankxpsuc  9877  tcrank  9879  cardlim  9967  cardaleph  10084  grur1  10815  elnnz  12568  elznn0  12573  elznn  12574  elxr  13096  xrrebnd  13147  xaddf  13203  xrinfmss  13289  elfzlmr  13746  ssnn0fi  13950  hashv01gt1  14305  hashtpg  14446  swrdnd2  14605  pfxnd0  14638  nofv  27160  nosepon  27168  tgldimor  27784  outpasch  28037  xrdifh  32022  eliccioo  32128  orngsqr  32453  elzdif0  32991  qqhval2lem  32992  dfso2  34756  dfon2lem5  34790  dfon2lem6  34791  ecase13d  35246  elicc3  35250  wl-df4-3mintru2  36416  wl-exeq  36451  dvasin  36620  4atlem3a  38516  4atlem3b  38517  frege133d  42564  or3or  42822  3ornot23VD  43656  xrssre  44106