Theorem 3orass 1104

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 1102	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
2		orass 934	. 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))

Syntax hints:   ↔ wb 209   ∨ wo 860   ∨ w3o 1100

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 210  df-or 861  df-3or 1102

This theorem is referenced by:  3orel1  1105  3orrot  1106  3orcoma  1107  3mix1  1347  ecase13d  1499  ecase23d  1500  3bior1fd  1503  cador  1635  moeq3  3682  sotric  5600  sotrieq  5601  isso2i  5607  ordzsl  7841  soxp  8125  frxp3  8147  wemapsolem  9512  rankxpsuc  9854  tcrank  9856  cardlim  9958  cardaleph  10073  grur1  10805  elnnz  12601  elznn0  12606  elznn  12607  elxr  13141  xrrebnd  13194  xaddf  13250  xrinfmss  13336  elfzlmr  13811  ssnn0fi  14021  hashv01gt1  14381  hashtpg  14522  swrdnd2  14693  pfxnd0  14726  chnccat  18682  orngsqr  20947  nofv  27787  nosepon  27795  elzs2  28558  elnnzs  28560  elznns  28561  tgldimor  28737  outpasch  28996  elplng  29020  lnincplng  29024  plngcplem  29025  plngrotlem2  29028  plngmiropp  29034  xrdifh  33066  eliccioo  33191  elzdif0  34315  qqhval2lem  34316  dfso2  36180  dfon2lem5  36210  dfon2lem6  36211  elicc3  36751  wl-df4-3mintru2  38056  wl-exeq  38112  dvasin  38278  4atlem3a  40296  4atlem3b  40297  frege133d  44418  or3or  44676  3ornot23VD  45482  xrssre  45991  usgrexmpl2nb0  48720  usgrexmpl2nb2  48722  usgrexmpl2nb3  48723  usgrexmpl2nb5  48725