Theorem 3orass 1088

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 1086	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 918	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 205   ∨ wo 843   ∨ w3o 1084

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 206  df-or 844  df-3or 1086

This theorem is referenced by:  3orel1  1089  3orrot  1090  3orcoma  1091  3mix1  1328  ecase23d  1471  3bior1fd  1473  cador  1611  moeq3  3642  sotric  5522  sotrieq  5523  isso2i  5529  ordzsl  7667  soxp  7941  wemapsolem  9239  rankxpsuc  9571  tcrank  9573  cardlim  9661  cardaleph  9776  grur1  10507  elnnz  12259  elznn0  12264  elznn  12265  elxr  12781  xrrebnd  12831  xaddf  12887  xrinfmss  12973  elfzlmr  13429  ssnn0fi  13633  hashv01gt1  13987  hashtpg  14127  swrdnd2  14296  pfxnd0  14329  tgldimor  26767  outpasch  27020  xrdifh  31003  eliccioo  31107  orngsqr  31405  elzdif0  31830  qqhval2lem  31831  dfso2  33628  dfon2lem5  33669  dfon2lem6  33670  frxp3  33724  nofv  33787  nosepon  33795  ecase13d  34429  elicc3  34433  wl-df4-3mintru2  35585  wl-exeq  35620  dvasin  35788  4atlem3a  37538  4atlem3b  37539  frege133d  41262  or3or  41520  3ornot23VD  42356  xrssre  42777