Theorem orcomd 648

Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)

Hypothesis

Ref	Expression
orcomd.1	|- ( ph -> ( ps \/ ch ) )

Assertion

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

Proof of Theorem orcomd

Step	Hyp	Ref	Expression
1		orcomd.1	. 2 |- ( ph -> ( ps \/ ch ) )
2		orcom 647	. 2 |- ( ( ps \/ ch ) <-> ( ch \/ ps ) )
3	1, 2	sylib 127	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  olcd  653  stabtestimpdc  824  pm5.54dc  827  swopo  4043  sotritrieq  4062  reg3exmidlemwe  4303  acexmidlemcase  5507  2oconcl  6022  nntri3or  6072  nntri2  6073  nntri1  6074  nnsseleq  6079  diffisn  6350  addnqprlemfu  6658  mulnqprlemfu  6674  addcanprlemu  6713  cauappcvgprlemladdru  6754  apreap  7578  mulap0r  7606  nnm1nn0  8223  elnn0z  8258  zleloe  8292  nneoor  8340  nneo  8341  zeo2  8344  uzm1  8503  nn01to3  8552  uzsplit  8954  fzospliti  9032  fzouzsplit  9035