Theorem orcomd 724

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

Syntax hints:   -> wi 4   \/ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  729  stdcndcOLD  841  pm5.54dc  913  r19.30dc  2617  exmid1dc  4186  swopo  4291  sotritrieq  4310  ontriexmidim  4506  ontri2orexmidim  4556  reg3exmidlemwe  4563  acexmidlemcase  5848  2oconcl  6418  nntri3or  6472  nntri2  6473  nntri1  6475  nnsseleq  6480  diffisn  6871  fival  6947  djulclb  7032  exmidomniim  7117  exmidomni  7118  omniwomnimkv  7143  nninfwlpoimlemginf  7152  exmidontriimlem1  7198  3nsssucpw1  7213  addnqprlemfu  7522  mulnqprlemfu  7538  addcanprlemu  7577  cauappcvgprlemladdru  7618  apreap  8506  mulap0r  8534  mul0eqap  8588  nnm1nn0  9176  elnn0z  9225  zleloe  9259  nneoor  9314  nneo  9315  zeo2  9318  uzm1  9517  nn01to3  9576  uzsplit  10048  fzospliti  10132  fzouzsplit  10135  qavgle  10215  xrmaxiflemlub  11211  fz1f1o  11338  fprodsplitdc  11559  fprodcl2lem  11568  ef0lem  11623  zeo3  11827  bezoutlemmain  11953  prmdc  12084  unennn  12352  exmidunben  12381  lgsval  13699  lgsfvalg  13700  lgsdilem  13722  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048  exmidsbthrlem  14054  sbthomlem  14057  trilpolemeq1  14072