Theorem orcomd 741

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

Syntax hints:   -> wi 4   \/ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4332  swopo  4446  sotritrieq  4465  ontriexmidim  4664  ontri2orexmidim  4714  reg3exmidlemwe  4721  acexmidlemcase  6070  2oconcl  6702  nntri3or  6756  nntri2  6757  nntri1  6759  nnsseleq  6764  diffisn  7187  fival  7294  djulclb  7385  exmidomniim  7471  exmidomni  7472  omniwomnimkv  7497  nninfwlpoimlemginf  7506  exmidontriimlem1  7567  3nsssucpw1  7585  addnqprlemfu  7917  mulnqprlemfu  7933  addcanprlemu  7972  cauappcvgprlemladdru  8013  apreap  8905  mulap0r  8933  mul0eqap  8990  nnm1nn0  9583  elnn0z  9636  zleloe  9670  nneoor  9727  nneo  9728  zeo2  9731  uzm1  9932  nn01to3  9996  uzsplit  10477  fzospliti  10563  fzouzsplit  10566  qavgle  10671  xrmaxiflemlub  11992  fz1f1o  12119  fprodsplitdc  12341  fprodcl2lem  12350  ef0lem  12405  zeo3  12613  bezoutlemmain  12753  nninfctlemfo  12795  prmdc  12886  unennn  13266  exmidunben  13295  fnpr2ob  13638  ivthdichlem  15675  plycoeid3  15781  lgsval  16037  lgsfvalg  16038  lgsdilem  16060  nninfalllem1  16956  nninfall  16957  nninfsellemqall  16963  nninfnfiinf  16971  exmidsbthrlem  16972  sbthomlem  16975  trilpolemeq1  16994