Theorem 3orass 861

Description: Associative law for triple disjunction.

Assertion

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

Proof of Theorem 3orass

Step	Hyp	Ref	Expression
1		df-3or 859	. 2 |- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
2		orass 280	. 2 |- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))
3	1, 2	bitri 190	1 |- ((ph \/ ps \/ ch) <-> (ph \/ (ps \/ ch)))

Syntax hints:   <-> wb 163   \/ wo 239   \/ w3o 857

This theorem is referenced by:  3orrot 864  3orcomb 867  3mix1 1045  ecase23d 1198  3ornot23 1281  eueq3 2430  moeq3 2432  sotric 3615  sotrieq 3616  so 3620  ordtri2orOLD 3767  dfwe2OLD 3862  ordzsl 3927  dfrdg2 5141  rankxpsuc 5826  infenomsub 5889  cardlim 6003  cardaleph 6033  elxr 6706  ssxrOLD 6715  xrrebnd 6743  xrinfmss 7288  elnnz 7354  0z 7355  elznn0 7358  elznn 7359  3orel1 13805  dfon2lem5 13853  dfon2lem6 13854  soxp 13950  nofv 13998  axfelem8 14038  ecase13d 15350  elicc3 15362  infenomsubOLD 15398  3ornot23VD 16671

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 164  df-or 241  df-3or 859

Copyright terms: Public domain