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  8915  mulap0r  8943  mul0eqap  9000  nnm1nn0  9604  elnn0z  9657  zleloe  9691  nneoor  9748  nneo  9749  zeo2  9752  uzm1  9953  nn01to3  10017  uzsplit  10499  fzospliti  10585  fzouzsplit  10588  qavgle  10693  xrmaxiflemlub  12014  fz1f1o  12141  fprodsplitdc  12363  fprodcl2lem  12372  ef0lem  12427  zeo3  12635  bezoutlemmain  12775  nninfctlemfo  12817  prmdc  12908  unennn  13288  exmidunben  13317  fnpr2ob  13661  ivthdichlem  15752  plycoeid3  15858  lgsval  16123  lgsfvalg  16124  lgsdilem  16146  wexmiddiffilem  17043  wexmiddifxylem  17045  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058  nninfnfiinf  17066  exmidsbthrlem  17067  sbthomlem  17070  trilpolemeq1  17089