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  3673  sotric  5597  sotrieq  5598  isso2i  5604  ordzsl  7844  soxp  8130  frxp3  8152  wemapsolem  9525  rankxpsuc  9867  tcrank  9869  cardlim  9980  cardaleph  10095  grur1  10832  elnnz  12628  elznn0  12633  elznn  12634  elxr  13169  xrrebnd  13222  xaddf  13278  xrinfmss  13364  elfzlmr  13840  ssnn0fi  14051  hashv01gt1  14411  hashtpg  14552  swrdnd2  14727  pfxnd0  14760  chnccat  18718  orngsqr  21033  nofv  27891  nosepon  27899  elzs2  28662  elnnzs  28664  elznns  28665  tgldimor  28842  outpasch  29110  elplng  29135  lnincplng  29139  plngcplem  29140  plngrotlem2  29143  plngmiropp  29149  xrdifh  33238  eliccioo  33363  elzdif0  34477  qqhval2lem  34478  dfso2  36321  dfon2lem5  36351  dfon2lem6  36352  elicc3  36923  wl-df4-3mintru2  38228  wl-exeq  38284  dvasin  38440  4atlem3a  40457  4atlem3b  40458  frege133d  44592  or3or  44850  3ornot23VD  45656  xrssre  46165  usgrexmpl2nb0  48934  usgrexmpl2nb2  48936  usgrexmpl2nb3  48937  usgrexmpl2nb5  48939