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  1329  ecase23d  1472  3bior1fd  1474  cador  1604  moeq3  3720  sotric  5625  sotrieq  5626  isso2i  5632  ordzsl  7865  soxp  8152  frxp3  8174  wemapsolem  9587  rankxpsuc  9919  tcrank  9921  cardlim  10009  cardaleph  10126  grur1  10857  elnnz  12620  elznn0  12625  elznn  12626  elxr  13155  xrrebnd  13206  xaddf  13262  xrinfmss  13348  elfzlmr  13816  ssnn0fi  14022  hashv01gt1  14380  hashtpg  14520  swrdnd2  14689  pfxnd0  14722  nofv  27716  nosepon  27724  elzs2  28399  elnnzs  28401  elznns  28402  tgldimor  28524  outpasch  28777  xrdifh  32788  eliccioo  32897  orngsqr  33313  elzdif0  33942  qqhval2lem  33943  dfso2  35734  dfon2lem5  35768  dfon2lem6  35769  ecase13d  36295  elicc3  36299  wl-df4-3mintru2  37469  wl-exeq  37514  dvasin  37690  4atlem3a  39579  4atlem3b  39580  frege133d  43754  or3or  44012  3ornot23VD  44844  xrssre  45297  usgrexmpl2nb0  47925  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb5  47930