Theorem orass 524

Description: Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
orass

Proof of Theorem orass

Step	Hyp	Ref	Expression
1		orcom 387	. 2
2		or12 523	. 2
3		orcom 387	. . 3
4	3	orbi2i 519	. 2
5	1, 2, 4	3bitri 271	1

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

This theorem is referenced by:  pm2.31  525  pm2.32  526  or32  527  or4  528  3orass  976  axi12  2433  unass  3660  tppreqb  4171  ltxr  11353  plydivex  22693  disjxpin  27447  impor  30478  lcmass  31218  bj-ifim123g  37706

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