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  4233  swopo  4341  sotritrieq  4360  ontriexmidim  4558  ontri2orexmidim  4608  reg3exmidlemwe  4615  acexmidlemcase  5917  2oconcl  6497  nntri3or  6551  nntri2  6552  nntri1  6554  nnsseleq  6559  diffisn  6954  fival  7036  djulclb  7121  exmidomniim  7207  exmidomni  7208  omniwomnimkv  7233  nninfwlpoimlemginf  7242  exmidontriimlem1  7288  3nsssucpw1  7303  addnqprlemfu  7627  mulnqprlemfu  7643  addcanprlemu  7682  cauappcvgprlemladdru  7723  apreap  8614  mulap0r  8642  mul0eqap  8697  nnm1nn0  9290  elnn0z  9339  zleloe  9373  nneoor  9428  nneo  9429  zeo2  9432  uzm1  9632  nn01to3  9691  uzsplit  10167  fzospliti  10252  fzouzsplit  10255  qavgle  10348  xrmaxiflemlub  11413  fz1f1o  11540  fprodsplitdc  11761  fprodcl2lem  11770  ef0lem  11825  zeo3  12033  bezoutlemmain  12165  nninfctlemfo  12207  prmdc  12298  unennn  12614  exmidunben  12643  fnpr2ob  12983  ivthdichlem  14887  plycoeid3  14993  lgsval  15245  lgsfvalg  15246  lgsdilem  15268  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659  exmidsbthrlem  15666  sbthomlem  15669  trilpolemeq1  15684