Theorem 3orass 1090

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 1088	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 920	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 205   ∨ wo 845   ∨ w3o 1086

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 206  df-or 846  df-3or 1088

This theorem is referenced by:  3orel1  1091  3orrot  1092  3orcoma  1093  3mix1  1330  ecase23d  1473  3bior1fd  1475  cador  1609  moeq3  3708  sotric  5616  sotrieq  5617  isso2i  5623  ordzsl  7833  soxp  8114  frxp3  8136  wemapsolem  9544  rankxpsuc  9876  tcrank  9878  cardlim  9966  cardaleph  10083  grur1  10814  elnnz  12567  elznn0  12572  elznn  12573  elxr  13095  xrrebnd  13146  xaddf  13202  xrinfmss  13288  elfzlmr  13745  ssnn0fi  13949  hashv01gt1  14304  hashtpg  14445  swrdnd2  14604  pfxnd0  14637  nofv  27157  nosepon  27165  tgldimor  27750  outpasch  28003  xrdifh  31986  eliccioo  32092  orngsqr  32417  elzdif0  32955  qqhval2lem  32956  dfso2  34720  dfon2lem5  34754  dfon2lem6  34755  ecase13d  35193  elicc3  35197  wl-df4-3mintru2  36363  wl-exeq  36398  dvasin  36567  4atlem3a  38463  4atlem3b  38464  frege133d  42506  or3or  42764  3ornot23VD  43598  xrssre  44048