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  1330  ecase23d  1474  3bior1fd  1476  cador  1607  moeq3  3700  sotric  5602  sotrieq  5603  isso2i  5609  ordzsl  7848  soxp  8136  frxp3  8158  wemapsolem  9572  rankxpsuc  9904  tcrank  9906  cardlim  9994  cardaleph  10111  grur1  10842  elnnz  12606  elznn0  12611  elznn  12612  elxr  13140  xrrebnd  13192  xaddf  13248  xrinfmss  13334  elfzlmr  13802  ssnn0fi  14008  hashv01gt1  14366  hashtpg  14506  swrdnd2  14675  pfxnd0  14708  nofv  27638  nosepon  27646  elzs2  28321  elnnzs  28323  elznns  28324  tgldimor  28446  outpasch  28699  xrdifh  32721  eliccioo  32853  orngsqr  33274  elzdif0  33940  qqhval2lem  33941  dfso2  35714  dfon2lem5  35747  dfon2lem6  35748  ecase13d  36273  elicc3  36277  wl-df4-3mintru2  37447  wl-exeq  37494  dvasin  37670  4atlem3a  39558  4atlem3b  39559  frege133d  43740  or3or  43998  3ornot23VD  44824  xrssre  45316  usgrexmpl2nb0  47948  usgrexmpl2nb2  47950  usgrexmpl2nb3  47951  usgrexmpl2nb5  47953