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  3658  sotric  5569  sotrieq  5570  isso2i  5576  ordzsl  7796  soxp  8079  frxp3  8101  wemapsolem  9465  rankxpsuc  9806  tcrank  9808  cardlim  9896  cardaleph  10011  grur1  10743  elnnz  12534  elznn0  12539  elznn  12540  elxr  13067  xrrebnd  13120  xaddf  13176  xrinfmss  13262  elfzlmr  13737  ssnn0fi  13947  hashv01gt1  14307  hashtpg  14447  swrdnd2  14618  pfxnd0  14651  chnccat  18592  orngsqr  20843  nofv  27621  nosepon  27629  elzs2  28391  elnnzs  28393  elznns  28394  tgldimor  28570  outpasch  28823  xrdifh  32853  eliccioo  32990  elzdif0  34124  qqhval2lem  34125  dfso2  35937  dfon2lem5  35967  dfon2lem6  35968  ecase13d  36495  elicc3  36499  wl-df4-3mintru2  37803  wl-exeq  37859  dvasin  38025  4atlem3a  40043  4atlem3b  40044  frege133d  44192  or3or  44450  3ornot23VD  45273  xrssre  45778  usgrexmpl2nb0  48507  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb5  48512