Theorem orcomd 736

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

Syntax hints:   -> wi 4   \/ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  741  stdcndcOLD  853  pm5.54dc  925  r19.30dc  2680  exmid1dc  4290  swopo  4403  sotritrieq  4422  ontriexmidim  4620  ontri2orexmidim  4670  reg3exmidlemwe  4677  acexmidlemcase  6013  2oconcl  6607  nntri3or  6661  nntri2  6662  nntri1  6664  nnsseleq  6669  diffisn  7082  fival  7169  djulclb  7254  exmidomniim  7340  exmidomni  7341  omniwomnimkv  7366  nninfwlpoimlemginf  7375  exmidontriimlem1  7436  3nsssucpw1  7454  addnqprlemfu  7780  mulnqprlemfu  7796  addcanprlemu  7835  cauappcvgprlemladdru  7876  apreap  8767  mulap0r  8795  mul0eqap  8850  nnm1nn0  9443  elnn0z  9492  zleloe  9526  nneoor  9582  nneo  9583  zeo2  9586  uzm1  9787  nn01to3  9851  uzsplit  10327  fzospliti  10413  fzouzsplit  10416  qavgle  10519  xrmaxiflemlub  11826  fz1f1o  11953  fprodsplitdc  12175  fprodcl2lem  12184  ef0lem  12239  zeo3  12447  bezoutlemmain  12587  nninfctlemfo  12629  prmdc  12720  unennn  13036  exmidunben  13065  fnpr2ob  13441  ivthdichlem  15394  plycoeid3  15500  lgsval  15752  lgsfvalg  15753  lgsdilem  15775  nninfalllem1  16661  nninfall  16662  nninfsellemqall  16668  nninfnfiinf  16676  exmidsbthrlem  16677  sbthomlem  16680  trilpolemeq1  16695