Theorem orass 260

Description: Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118.

Assertion

Ref	Expression
orass	|- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))

Proof of Theorem orass

Step	Hyp	Ref	Expression
1		or12 258	. 2 |- ((ch \/ (ph \/ ps)) <-> (ph \/ (ch \/ ps)))
2		orcom 246	. 2 |- (((ph \/ ps) \/ ch) <-> (ch \/ (ph \/ ps)))
3		orcom 246	. . 3 |- ((ps \/ ch) <-> (ch \/ ps))
4	3	orbi2i 255	. 2 |- ((ph \/ (ps \/ ch)) <-> (ph \/ (ch \/ ps)))
5	1, 2, 4	3bitr4 183	1 |- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))

Syntax hints:   <-> wb 146   \/ wo 222

This theorem is referenced by:  pm2.31 261  pm2.32 262  or23 263  or4 264  3orass 777  eueq3 1915  unass 2183  ltxrltt 5480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain