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  1331  ecase23d  1475  3bior1fd  1477  cador  1608  moeq3  3718  sotric  5622  sotrieq  5623  isso2i  5629  ordzsl  7866  soxp  8154  frxp3  8176  wemapsolem  9590  rankxpsuc  9922  tcrank  9924  cardlim  10012  cardaleph  10129  grur1  10860  elnnz  12623  elznn0  12628  elznn  12629  elxr  13158  xrrebnd  13210  xaddf  13266  xrinfmss  13352  elfzlmr  13820  ssnn0fi  14026  hashv01gt1  14384  hashtpg  14524  swrdnd2  14693  pfxnd0  14726  nofv  27702  nosepon  27710  elzs2  28385  elnnzs  28387  elznns  28388  tgldimor  28510  outpasch  28763  xrdifh  32782  eliccioo  32913  orngsqr  33334  elzdif0  33981  qqhval2lem  33982  dfso2  35755  dfon2lem5  35788  dfon2lem6  35789  ecase13d  36314  elicc3  36318  wl-df4-3mintru2  37488  wl-exeq  37535  dvasin  37711  4atlem3a  39599  4atlem3b  39600  frege133d  43778  or3or  44036  3ornot23VD  44867  xrssre  45359  usgrexmpl2nb0  47990  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb5  47995