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  3671  sotric  5563  sotrieq  5564  isso2i  5570  ordzsl  7789  soxp  8073  frxp3  8095  wemapsolem  9459  rankxpsuc  9798  tcrank  9800  cardlim  9888  cardaleph  10003  grur1  10735  elnnz  12502  elznn0  12507  elznn  12508  elxr  13034  xrrebnd  13087  xaddf  13143  xrinfmss  13229  elfzlmr  13702  ssnn0fi  13912  hashv01gt1  14272  hashtpg  14412  swrdnd2  14583  pfxnd0  14616  chnccat  18553  orngsqr  20803  nofv  27629  nosepon  27637  elzs2  28399  elnnzs  28401  elznns  28402  tgldimor  28578  outpasch  28831  xrdifh  32862  eliccioo  33014  elzdif0  34139  qqhval2lem  34140  dfso2  35951  dfon2lem5  35981  dfon2lem6  35982  ecase13d  36509  elicc3  36513  wl-df4-3mintru2  37694  wl-exeq  37741  dvasin  37907  4atlem3a  39925  4atlem3b  39926  frege133d  44073  or3or  44331  3ornot23VD  45154  xrssre  45660  usgrexmpl2nb0  48344  usgrexmpl2nb2  48346  usgrexmpl2nb3  48347  usgrexmpl2nb5  48349