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

Syntax hints:   ↔ wb 206   ∨ wo 846   ∨ 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 847  df-3or 1088

This theorem is referenced by:  3orel1  1091  3orrot  1092  3orcoma  1093  3mix1  1330  ecase23d  1473  3bior1fd  1475  cador  1605  moeq3  3734  sotric  5637  sotrieq  5638  isso2i  5644  ordzsl  7882  soxp  8170  frxp3  8192  wemapsolem  9619  rankxpsuc  9951  tcrank  9953  cardlim  10041  cardaleph  10158  grur1  10889  elnnz  12649  elznn0  12654  elznn  12655  elxr  13179  xrrebnd  13230  xaddf  13286  xrinfmss  13372  elfzlmr  13831  ssnn0fi  14036  hashv01gt1  14394  hashtpg  14534  swrdnd2  14703  pfxnd0  14736  nofv  27720  nosepon  27728  elzs2  28403  elnnzs  28405  elznns  28406  tgldimor  28528  outpasch  28781  xrdifh  32785  eliccioo  32895  orngsqr  33299  elzdif0  33926  qqhval2lem  33927  dfso2  35717  dfon2lem5  35751  dfon2lem6  35752  ecase13d  36279  elicc3  36283  wl-df4-3mintru2  37453  wl-exeq  37488  dvasin  37664  4atlem3a  39554  4atlem3b  39555  frege133d  43727  or3or  43985  3ornot23VD  44818  xrssre  45263  usgrexmpl2nb0  47846  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb5  47851