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  7396  exmidomniim  7482  exmidomni  7483  omniwomnimkv  7508  nninfwlpoimlemginf  7517  exmidontriimlem1  7578  3nsssucpw1  7596  addnqprlemfu  7928  mulnqprlemfu  7944  addcanprlemu  7983  cauappcvgprlemladdru  8024  apreap  8918  mulap0r  8946  mul0eqap  9003  nnm1nn0  9609  elnn0z  9662  zleloe  9696  nneoor  9753  nneo  9754  zeo2  9757  uzm1  9963  nn01to3  10027  uzsplit  10510  fzospliti  10596  fzouzsplit  10599  qavgle  10704  xrmaxiflemlub  12033  fz1f1o  12160  fprodsplitdc  12382  fprodcl2lem  12391  ef0lem  12446  zeo3  12654  bezoutlemmain  12794  nninfctlemfo  12836  prmdc  12927  unennn  13340  exmidunben  13369  fnpr2ob  13714  ivthdichlem  15843  plycoeid3  15949  lgsval  16289  lgsfvalg  16290  lgsdilem  16312  wexmiddiffilem  17209  wexmiddifxylem  17211  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224  nninfnfiinf  17232  exmidsbthrlem  17233  sbthomlem  17236  trilpolemeq1  17256