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 ) )

This proof depends on syntax axioms:   -> wi 4   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  olcd  746  stdcndcOLD  858  pm5.54dc  930  r19.30dc  2698  exmid1dc  4337  swopo  4451  sotritrieq  4470  ontriexmidim  4669  ontri2orexmidim  4719  reg3exmidlemwe  4726  acexmidlemcase  6080  2oconcl  6712  nntri3or  6766  nntri2  6767  nntri1  6769  nnsseleq  6774  diffisn  7197  fival  7304  djulclb  7395  exmidomniim  7481  exmidomni  7482  omniwomnimkv  7507  nninfwlpoimlemginf  7516  exmidontriimlem1  7577  3nsssucpw1  7595  addnqprlemfu  7927  mulnqprlemfu  7943  addcanprlemu  7982  cauappcvgprlemladdru  8023  apreap  8917  mulap0r  8945  mul0eqap  9002  nnm1nn0  9608  elnn0z  9661  zleloe  9695  nneoor  9752  nneo  9753  zeo2  9756  uzm1  9962  nn01to3  10026  uzsplit  10509  fzospliti  10595  fzouzsplit  10598  qavgle  10703  xrmaxiflemlub  12030  fz1f1o  12157  fprodsplitdc  12379  fprodcl2lem  12388  ef0lem  12443  zeo3  12651  bezoutlemmain  12791  nninfctlemfo  12833  prmdc  12924  unennn  13337  exmidunben  13366  fnpr2ob  13710  ivthdichlem  15801  plycoeid3  15907  lgsval  16221  lgsfvalg  16222  lgsdilem  16244  wexmiddiffilem  17141  wexmiddifxylem  17143  nninfalllem1  17149  nninfall  17150  nninfsellemqall  17156  nninfnfiinf  17164  exmidsbthrlem  17165  sbthomlem  17168  trilpolemeq1  17187