Theorem 3orass 1090

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

Syntax hints:   ↔ wb 206   ∨ wo 848   ∨ w3o 1086

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 849  df-3or 1088

This theorem is referenced by:  3orel1  1091  3orrot  1092  3orcoma  1093  3mix1  1332  ecase23d  1476  3bior1fd  1478  cador  1610  moeq3  3659  sotric  5564  sotrieq  5565  isso2i  5571  ordzsl  7791  soxp  8074  frxp3  8096  wemapsolem  9460  rankxpsuc  9801  tcrank  9803  cardlim  9891  cardaleph  10006  grur1  10738  elnnz  12529  elznn0  12534  elznn  12535  elxr  13062  xrrebnd  13115  xaddf  13171  xrinfmss  13257  elfzlmr  13732  ssnn0fi  13942  hashv01gt1  14302  hashtpg  14442  swrdnd2  14613  pfxnd0  14646  chnccat  18587  orngsqr  20838  nofv  27639  nosepon  27647  elzs2  28409  elnnzs  28411  elznns  28412  tgldimor  28588  outpasch  28841  xrdifh  32872  eliccioo  33009  elzdif0  34144  qqhval2lem  34145  dfso2  35957  dfon2lem5  35987  dfon2lem6  35988  ecase13d  36515  elicc3  36519  wl-df4-3mintru2  37823  wl-exeq  37879  dvasin  38045  4atlem3a  40063  4atlem3b  40064  frege133d  44216  or3or  44474  3ornot23VD  45297  xrssre  45802  usgrexmpl2nb0  48525  usgrexmpl2nb2  48527  usgrexmpl2nb3  48528  usgrexmpl2nb5  48530