Theorem orcomd 731

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

Syntax hints:   -> wi 4   \/ wo 710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  736  stdcndcOLD  848  pm5.54dc  920  r19.30dc  2654  exmid1dc  4251  swopo  4360  sotritrieq  4379  ontriexmidim  4577  ontri2orexmidim  4627  reg3exmidlemwe  4634  acexmidlemcase  5951  2oconcl  6537  nntri3or  6591  nntri2  6592  nntri1  6594  nnsseleq  6599  diffisn  7004  fival  7086  djulclb  7171  exmidomniim  7257  exmidomni  7258  omniwomnimkv  7283  nninfwlpoimlemginf  7292  exmidontriimlem1  7348  3nsssucpw1  7363  addnqprlemfu  7688  mulnqprlemfu  7704  addcanprlemu  7743  cauappcvgprlemladdru  7784  apreap  8675  mulap0r  8703  mul0eqap  8758  nnm1nn0  9351  elnn0z  9400  zleloe  9434  nneoor  9490  nneo  9491  zeo2  9494  uzm1  9694  nn01to3  9753  uzsplit  10229  fzospliti  10315  fzouzsplit  10318  qavgle  10418  xrmaxiflemlub  11629  fz1f1o  11756  fprodsplitdc  11977  fprodcl2lem  11986  ef0lem  12041  zeo3  12249  bezoutlemmain  12389  nninfctlemfo  12431  prmdc  12522  unennn  12838  exmidunben  12867  fnpr2ob  13242  ivthdichlem  15193  plycoeid3  15299  lgsval  15551  lgsfvalg  15552  lgsdilem  15574  nninfalllem1  16080  nninfall  16081  nninfsellemqall  16087  nninfnfiinf  16095  exmidsbthrlem  16096  sbthomlem  16099  trilpolemeq1  16114