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  3672  sotric  5572  sotrieq  5573  isso2i  5579  ordzsl  7799  soxp  8083  frxp3  8105  wemapsolem  9469  rankxpsuc  9808  tcrank  9810  cardlim  9898  cardaleph  10013  grur1  10745  elnnz  12512  elznn0  12517  elznn  12518  elxr  13044  xrrebnd  13097  xaddf  13153  xrinfmss  13239  elfzlmr  13712  ssnn0fi  13922  hashv01gt1  14282  hashtpg  14422  swrdnd2  14593  pfxnd0  14626  chnccat  18563  orngsqr  20816  nofv  27642  nosepon  27650  elzs2  28412  elnnzs  28414  elznns  28415  tgldimor  28592  outpasch  28845  xrdifh  32877  eliccioo  33029  elzdif0  34164  qqhval2lem  34165  dfso2  35977  dfon2lem5  36007  dfon2lem6  36008  ecase13d  36535  elicc3  36539  wl-df4-3mintru2  37769  wl-exeq  37818  dvasin  37984  4atlem3a  40002  4atlem3b  40003  frege133d  44150  or3or  44408  3ornot23VD  45231  xrssre  45736  usgrexmpl2nb0  48420  usgrexmpl2nb2  48422  usgrexmpl2nb3  48423  usgrexmpl2nb5  48425