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  1331  ecase23d  1475  3bior1fd  1477  cador  1608  moeq3  3680  sotric  5569  sotrieq  5570  isso2i  5576  ordzsl  7801  soxp  8085  frxp3  8107  wemapsolem  9479  rankxpsuc  9811  tcrank  9813  cardlim  9901  cardaleph  10018  grur1  10749  elnnz  12515  elznn0  12520  elznn  12521  elxr  13052  xrrebnd  13104  xaddf  13160  xrinfmss  13246  elfzlmr  13718  ssnn0fi  13926  hashv01gt1  14286  hashtpg  14426  swrdnd2  14596  pfxnd0  14629  orngsqr  20786  nofv  27602  nosepon  27610  elzs2  28327  elnnzs  28329  elznns  28330  tgldimor  28482  outpasch  28735  xrdifh  32753  eliccioo  32901  elzdif0  33963  qqhval2lem  33964  dfso2  35735  dfon2lem5  35768  dfon2lem6  35769  ecase13d  36294  elicc3  36298  wl-df4-3mintru2  37468  wl-exeq  37515  dvasin  37691  4atlem3a  39584  4atlem3b  39585  frege133d  43747  or3or  44005  3ornot23VD  44829  xrssre  45337  usgrexmpl2nb0  48015  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb5  48020