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  3695  sotric  5591  sotrieq  5592  isso2i  5598  ordzsl  7840  soxp  8128  frxp3  8150  wemapsolem  9564  rankxpsuc  9896  tcrank  9898  cardlim  9986  cardaleph  10103  grur1  10834  elnnz  12598  elznn0  12603  elznn  12604  elxr  13132  xrrebnd  13184  xaddf  13240  xrinfmss  13326  elfzlmr  13797  ssnn0fi  14003  hashv01gt1  14363  hashtpg  14503  swrdnd2  14673  pfxnd0  14706  nofv  27621  nosepon  27629  elzs2  28339  elnnzs  28341  elznns  28342  tgldimor  28481  outpasch  28734  xrdifh  32757  eliccioo  32905  orngsqr  33326  elzdif0  34011  qqhval2lem  34012  dfso2  35772  dfon2lem5  35805  dfon2lem6  35806  ecase13d  36331  elicc3  36335  wl-df4-3mintru2  37505  wl-exeq  37552  dvasin  37728  4atlem3a  39616  4atlem3b  39617  frege133d  43789  or3or  44047  3ornot23VD  44871  xrssre  45375  usgrexmpl2nb0  48035  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2nb5  48040