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  6012  2oconcl  6606  nntri3or  6660  nntri2  6661  nntri1  6663  nnsseleq  6668  diffisn  7081  fival  7168  djulclb  7253  exmidomniim  7339  exmidomni  7340  omniwomnimkv  7365  nninfwlpoimlemginf  7374  exmidontriimlem1  7435  3nsssucpw1  7453  addnqprlemfu  7779  mulnqprlemfu  7795  addcanprlemu  7834  cauappcvgprlemladdru  7875  apreap  8766  mulap0r  8794  mul0eqap  8849  nnm1nn0  9442  elnn0z  9491  zleloe  9525  nneoor  9581  nneo  9582  zeo2  9585  uzm1  9786  nn01to3  9850  uzsplit  10326  fzospliti  10412  fzouzsplit  10415  qavgle  10517  xrmaxiflemlub  11808  fz1f1o  11935  fprodsplitdc  12156  fprodcl2lem  12165  ef0lem  12220  zeo3  12428  bezoutlemmain  12568  nninfctlemfo  12610  prmdc  12701  unennn  13017  exmidunben  13046  fnpr2ob  13422  ivthdichlem  15374  plycoeid3  15480  lgsval  15732  lgsfvalg  15733  lgsdilem  15755  nninfalllem1  16610  nninfall  16611  nninfsellemqall  16617  nninfnfiinf  16625  exmidsbthrlem  16626  sbthomlem  16629  trilpolemeq1  16644