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  9813  tcrank  9815  cardlim  9903  cardaleph  10020  grur1  10751  elnnz  12517  elznn0  12522  elznn  12523  elxr  13054  xrrebnd  13106  xaddf  13162  xrinfmss  13248  elfzlmr  13720  ssnn0fi  13928  hashv01gt1  14288  hashtpg  14428  swrdnd2  14598  pfxnd0  14631  orngsqr  20787  nofv  27603  nosepon  27611  elzs2  28328  elnnzs  28330  elznns  28331  tgldimor  28483  outpasch  28736  xrdifh  32754  eliccioo  32902  elzdif0  33964  qqhval2lem  33965  dfso2  35736  dfon2lem5  35769  dfon2lem6  35770  ecase13d  36295  elicc3  36299  wl-df4-3mintru2  37469  wl-exeq  37516  dvasin  37692  4atlem3a  39585  4atlem3b  39586  frege133d  43748  or3or  44006  3ornot23VD  44830  xrssre  45338  usgrexmpl2nb0  48016  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb5  48021