Theorem 3orass 1106

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 1104	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 935	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  3orel1  1107  3orrot  1108  3orcoma  1109  3mix1  1349  ecase13d  1503  ecase23d  1504  3bior1fd  1507  cador  1641  moeq3  3673  sotric  5593  sotrieq  5594  isso2i  5600  ordzsl  7877  soxp  8165  frxp3  8192  wemapsolem  9568  rankxpsuc  9923  tcrank  9925  cardlim  10077  cardaleph  10192  grur1  10929  elnnz  12727  elznn0  12732  elznn  12733  elxr  13269  xrrebnd  13322  xaddf  13378  xrinfmss  13464  elfzlmr  13941  ssnn0fi  14152  hashv01gt1  14513  hashtpg  14654  swrdnd2  14830  pfxnd0  14863  chnccat  18826  orngsqr  21150  nofv  28041  nosepon  28049  elzs2  28812  elnnzs  28814  elznns  28815  tgldimor  28992  outpasch  29260  elplng  29285  lnincplng  29289  plngcplem  29290  plngrotlem2  29293  plngmiropp  29299  xrdifh  33439  eliccioo  33564  elzdif0  34679  qqhval2lem  34680  dfso2  36697  dfon2lem5  36726  dfon2lem6  36727  elicc3  37282  wl-df4-3mintru2  38601  wl-exeq  38657  dvasin  38813  4atlem3a  40845  4atlem3b  40846  frege133d  44955  or3or  45213  3ornot23VD  46018  xrssre  46563  usgrexmpl2nb0  49332  usgrexmpl2nb2  49334  usgrexmpl2nb3  49335  usgrexmpl2nb5  49337