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  3672  sotric  5557  sotrieq  5558  isso2i  5564  ordzsl  7778  soxp  8062  frxp3  8084  wemapsolem  9442  rankxpsuc  9778  tcrank  9780  cardlim  9868  cardaleph  9983  grur1  10714  elnnz  12481  elznn0  12486  elznn  12487  elxr  13018  xrrebnd  13070  xaddf  13126  xrinfmss  13212  elfzlmr  13684  ssnn0fi  13892  hashv01gt1  14252  hashtpg  14392  swrdnd2  14562  pfxnd0  14595  orngsqr  20751  nofv  27567  nosepon  27575  elzs2  28294  elnnzs  28296  elznns  28297  tgldimor  28451  outpasch  28704  xrdifh  32732  eliccioo  32880  elzdif0  33963  qqhval2lem  33964  dfso2  35748  dfon2lem5  35781  dfon2lem6  35782  ecase13d  36307  elicc3  36311  wl-df4-3mintru2  37481  wl-exeq  37528  dvasin  37704  4atlem3a  39596  4atlem3b  39597  frege133d  43758  or3or  44016  3ornot23VD  44840  xrssre  45348  usgrexmpl2nb0  48035  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2nb5  48040