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  3669  sotric  5561  sotrieq  5562  isso2i  5568  ordzsl  7787  soxp  8071  frxp3  8093  wemapsolem  9457  rankxpsuc  9796  tcrank  9798  cardlim  9886  cardaleph  10001  grur1  10733  elnnz  12500  elznn0  12505  elznn  12506  elxr  13032  xrrebnd  13085  xaddf  13141  xrinfmss  13227  elfzlmr  13700  ssnn0fi  13910  hashv01gt1  14270  hashtpg  14410  swrdnd2  14581  pfxnd0  14614  chnccat  18551  orngsqr  20801  nofv  27627  nosepon  27635  elzs2  28376  elnnzs  28378  elznns  28379  tgldimor  28555  outpasch  28808  xrdifh  32839  eliccioo  32991  elzdif0  34116  qqhval2lem  34117  dfso2  35928  dfon2lem5  35958  dfon2lem6  35959  ecase13d  36486  elicc3  36490  wl-df4-3mintru2  37661  wl-exeq  37708  dvasin  37874  4atlem3a  39892  4atlem3b  39893  frege133d  44043  or3or  44301  3ornot23VD  45124  xrssre  45630  usgrexmpl2nb0  48314  usgrexmpl2nb2  48316  usgrexmpl2nb3  48317  usgrexmpl2nb5  48319