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  1502  ecase23d  1503  3bior1fd  1506  cador  1641  moeq3  3669  sotric  5585  sotrieq  5586  isso2i  5592  ordzsl  7839  soxp  8124  frxp3  8146  wemapsolem  9522  rankxpsuc  9872  tcrank  9874  cardlim  10024  cardaleph  10139  grur1  10876  elnnz  12672  elznn0  12677  elznn  12678  elxr  13214  xrrebnd  13267  xaddf  13323  xrinfmss  13409  elfzlmr  13885  ssnn0fi  14096  hashv01gt1  14456  hashtpg  14597  swrdnd2  14772  pfxnd0  14805  chnccat  18761  orngsqr  21084  nofv  27947  nosepon  27955  elzs2  28718  elnnzs  28720  elznns  28721  tgldimor  28898  outpasch  29166  elplng  29191  lnincplng  29195  plngcplem  29196  plngrotlem2  29199  plngmiropp  29205  xrdifh  33305  eliccioo  33430  elzdif0  34545  qqhval2lem  34546  dfso2  36441  dfon2lem5  36471  dfon2lem6  36472  elicc3  37027  wl-df4-3mintru2  38330  wl-exeq  38386  dvasin  38542  4atlem3a  40574  4atlem3b  40575  frege133d  44709  or3or  44967  3ornot23VD  45773  xrssre  46282  usgrexmpl2nb0  49051  usgrexmpl2nb2  49053  usgrexmpl2nb3  49054  usgrexmpl2nb5  49056