Theorem orcomd 681

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 680	. 2 |- ( ( ps \/ ch ) <-> ( ch \/ ps ) )
3	1, 2	sylib 120	1 |- ( ph -> ( ch \/ ps ) )

Syntax hints:   -> wi 4   \/ wo 662

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  olcd  686  stabtestimpdc  858  pm5.54dc  861  swopo  4096  sotritrieq  4115  reg3exmidlemwe  4356  acexmidlemcase  5584  2oconcl  6133  nntri3or  6184  nntri2  6185  nntri1  6187  nnsseleq  6192  diffisn  6537  djulclb  6652  exmidomniim  6700  exmidomni  6701  addnqprlemfu  7020  mulnqprlemfu  7036  addcanprlemu  7075  cauappcvgprlemladdru  7116  apreap  7962  mulap0r  7990  nnm1nn0  8604  elnn0z  8657  zleloe  8691  nneoor  8742  nneo  8743  zeo2  8746  uzm1  8942  nn01to3  8995  uzsplit  9397  fzospliti  9474  fzouzsplit  9477  qavgle  9557  fz1f1o  10570  zeo3  10646  bezoutlemmain  10765  unennn  10988