Theorem orcomd 734

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

Syntax hints:   -> wi 4   \/ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  739  stdcndcOLD  851  pm5.54dc  923  r19.30dc  2678  exmid1dc  4283  swopo  4394  sotritrieq  4413  ontriexmidim  4611  ontri2orexmidim  4661  reg3exmidlemwe  4668  acexmidlemcase  5989  2oconcl  6575  nntri3or  6629  nntri2  6630  nntri1  6632  nnsseleq  6637  diffisn  7043  fival  7125  djulclb  7210  exmidomniim  7296  exmidomni  7297  omniwomnimkv  7322  nninfwlpoimlemginf  7331  exmidontriimlem1  7391  3nsssucpw1  7409  addnqprlemfu  7735  mulnqprlemfu  7751  addcanprlemu  7790  cauappcvgprlemladdru  7831  apreap  8722  mulap0r  8750  mul0eqap  8805  nnm1nn0  9398  elnn0z  9447  zleloe  9481  nneoor  9537  nneo  9538  zeo2  9541  uzm1  9741  nn01to3  9800  uzsplit  10276  fzospliti  10362  fzouzsplit  10365  qavgle  10465  xrmaxiflemlub  11745  fz1f1o  11872  fprodsplitdc  12093  fprodcl2lem  12102  ef0lem  12157  zeo3  12365  bezoutlemmain  12505  nninfctlemfo  12547  prmdc  12638  unennn  12954  exmidunben  12983  fnpr2ob  13359  ivthdichlem  15310  plycoeid3  15416  lgsval  15668  lgsfvalg  15669  lgsdilem  15691  nninfalllem1  16305  nninfall  16306  nninfsellemqall  16312  nninfnfiinf  16320  exmidsbthrlem  16321  sbthomlem  16324  trilpolemeq1  16339