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  4284  swopo  4397  sotritrieq  4416  ontriexmidim  4614  ontri2orexmidim  4664  reg3exmidlemwe  4671  acexmidlemcase  6002  2oconcl  6593  nntri3or  6647  nntri2  6648  nntri1  6650  nnsseleq  6655  diffisn  7063  fival  7148  djulclb  7233  exmidomniim  7319  exmidomni  7320  omniwomnimkv  7345  nninfwlpoimlemginf  7354  exmidontriimlem1  7414  3nsssucpw1  7432  addnqprlemfu  7758  mulnqprlemfu  7774  addcanprlemu  7813  cauappcvgprlemladdru  7854  apreap  8745  mulap0r  8773  mul0eqap  8828  nnm1nn0  9421  elnn0z  9470  zleloe  9504  nneoor  9560  nneo  9561  zeo2  9564  uzm1  9765  nn01to3  9824  uzsplit  10300  fzospliti  10386  fzouzsplit  10389  qavgle  10490  xrmaxiflemlub  11775  fz1f1o  11902  fprodsplitdc  12123  fprodcl2lem  12132  ef0lem  12187  zeo3  12395  bezoutlemmain  12535  nninfctlemfo  12577  prmdc  12668  unennn  12984  exmidunben  13013  fnpr2ob  13389  ivthdichlem  15341  plycoeid3  15447  lgsval  15699  lgsfvalg  15700  lgsdilem  15722  nninfalllem1  16462  nninfall  16463  nninfsellemqall  16469  nninfnfiinf  16477  exmidsbthrlem  16478  sbthomlem  16481  trilpolemeq1  16496