Theorem 3orass 1089

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  3orel1  1090  3orrot  1091  3orcoma  1092  3mix1  1331  ecase23d  1475  3bior1fd  1477  cador  1608  moeq3  3686  sotric  5579  sotrieq  5580  isso2i  5586  ordzsl  7824  soxp  8111  frxp3  8133  wemapsolem  9510  rankxpsuc  9842  tcrank  9844  cardlim  9932  cardaleph  10049  grur1  10780  elnnz  12546  elznn0  12551  elznn  12552  elxr  13083  xrrebnd  13135  xaddf  13191  xrinfmss  13277  elfzlmr  13749  ssnn0fi  13957  hashv01gt1  14317  hashtpg  14457  swrdnd2  14627  pfxnd0  14660  nofv  27576  nosepon  27584  elzs2  28294  elnnzs  28296  elznns  28297  tgldimor  28436  outpasch  28689  xrdifh  32710  eliccioo  32858  orngsqr  33289  elzdif0  33977  qqhval2lem  33978  dfso2  35749  dfon2lem5  35782  dfon2lem6  35783  ecase13d  36308  elicc3  36312  wl-df4-3mintru2  37482  wl-exeq  37529  dvasin  37705  4atlem3a  39598  4atlem3b  39599  frege133d  43761  or3or  44019  3ornot23VD  44843  xrssre  45351  usgrexmpl2nb0  48026  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb5  48031