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  1609  moeq3  3666  sotric  5552  sotrieq  5553  isso2i  5559  ordzsl  7775  soxp  8059  frxp3  8081  wemapsolem  9436  rankxpsuc  9775  tcrank  9777  cardlim  9865  cardaleph  9980  grur1  10711  elnnz  12478  elznn0  12483  elznn  12484  elxr  13015  xrrebnd  13067  xaddf  13123  xrinfmss  13209  elfzlmr  13682  ssnn0fi  13892  hashv01gt1  14252  hashtpg  14392  swrdnd2  14563  pfxnd0  14596  chnccat  18532  orngsqr  20781  nofv  27596  nosepon  27604  elzs2  28323  elnnzs  28325  elznns  28326  tgldimor  28480  outpasch  28733  xrdifh  32763  eliccioo  32911  elzdif0  33993  qqhval2lem  33994  dfso2  35799  dfon2lem5  35829  dfon2lem6  35830  ecase13d  36357  elicc3  36361  wl-df4-3mintru2  37531  wl-exeq  37578  dvasin  37743  4atlem3a  39695  4atlem3b  39696  frege133d  43857  or3or  44115  3ornot23VD  44938  xrssre  45446  usgrexmpl2nb0  48130  usgrexmpl2nb2  48132  usgrexmpl2nb3  48133  usgrexmpl2nb5  48135