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  3659  sotric  5560  sotrieq  5561  isso2i  5567  ordzsl  7787  soxp  8070  frxp3  8092  wemapsolem  9456  rankxpsuc  9795  tcrank  9797  cardlim  9885  cardaleph  10000  grur1  10732  elnnz  12523  elznn0  12528  elznn  12529  elxr  13056  xrrebnd  13109  xaddf  13165  xrinfmss  13251  elfzlmr  13726  ssnn0fi  13936  hashv01gt1  14296  hashtpg  14436  swrdnd2  14607  pfxnd0  14640  chnccat  18581  orngsqr  20832  nofv  27640  nosepon  27648  elzs2  28410  elnnzs  28412  elznns  28413  tgldimor  28589  outpasch  28842  xrdifh  32873  eliccioo  33010  elzdif0  34145  qqhval2lem  34146  dfso2  35958  dfon2lem5  35988  dfon2lem6  35989  ecase13d  36516  elicc3  36520  wl-df4-3mintru2  37814  wl-exeq  37870  dvasin  38036  4atlem3a  40054  4atlem3b  40055  frege133d  44207  or3or  44465  3ornot23VD  45288  xrssre  45793  usgrexmpl2nb0  48504  usgrexmpl2nb2  48506  usgrexmpl2nb3  48507  usgrexmpl2nb5  48509