Theorem orcomd 730

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

Syntax hints:   -> wi 4   \/ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  735  stdcndcOLD  847  pm5.54dc  919  r19.30dc  2644  exmid1dc  4234  swopo  4342  sotritrieq  4361  ontriexmidim  4559  ontri2orexmidim  4609  reg3exmidlemwe  4616  acexmidlemcase  5920  2oconcl  6506  nntri3or  6560  nntri2  6561  nntri1  6563  nnsseleq  6568  diffisn  6963  fival  7045  djulclb  7130  exmidomniim  7216  exmidomni  7217  omniwomnimkv  7242  nninfwlpoimlemginf  7251  exmidontriimlem1  7304  3nsssucpw1  7319  addnqprlemfu  7644  mulnqprlemfu  7660  addcanprlemu  7699  cauappcvgprlemladdru  7740  apreap  8631  mulap0r  8659  mul0eqap  8714  nnm1nn0  9307  elnn0z  9356  zleloe  9390  nneoor  9445  nneo  9446  zeo2  9449  uzm1  9649  nn01to3  9708  uzsplit  10184  fzospliti  10269  fzouzsplit  10272  qavgle  10365  xrmaxiflemlub  11430  fz1f1o  11557  fprodsplitdc  11778  fprodcl2lem  11787  ef0lem  11842  zeo3  12050  bezoutlemmain  12190  nninfctlemfo  12232  prmdc  12323  unennn  12639  exmidunben  12668  fnpr2ob  13042  ivthdichlem  14971  plycoeid3  15077  lgsval  15329  lgsfvalg  15330  lgsdilem  15352  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746  exmidsbthrlem  15753  sbthomlem  15756  trilpolemeq1  15771