Theorem 3orass 976

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 974	. 2
2		orass 524	. 2
3	1, 2	bitri 249	1

Syntax hints:  <->wb 184  \/wo 368  \/w3o 972

This theorem is referenced by:  3orrot  979  3orcoma  981  3orcomb  983  3mix1  1165  ecase23d  1332  3bior1fd  1334  cador  1458  moeq3  3276  sotric  4831  sotrieq  4832  isso2i  4837  ordzsl  6680  soxp  6913  wemapsolem  7996  rankxpsuc  8321  tcrank  8323  cardlim  8374  cardaleph  8491  grur1  9219  elnnz  10899  elznn0  10904  elznn  10905  elxr  11354  xrrebnd  11398  xaddf  11452  xrinfmss  11530  ssnn0fi  12094  hashv01gt1  12418  hashtpg  12523  swrdvalodm2  12664  swrdvalodm  12665  tgldimor  23893  xrdifh  27591  eliccioo  27627  orngsqr  27794  elzdif0  27961  qqhval2lem  27962  3orel1  29087  dfso2  29183  socnv  29194  dfon2lem5  29219  dfon2lem6  29220  nofv  29417  nobndup  29460  wl-exeq  29987  dvasin  30103  ecase13d  30131  elicc3  30135  3ornot23VD  33647  4atlem3a  35321  4atlem3b  35322

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 185  df-or 370  df-3or 974