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  4339  swopo  4453  sotritrieq  4472  ontriexmidim  4671  ontri2orexmidim  4721  reg3exmidlemwe  4728  acexmidlemcase  6083  2oconcl  6716  nntri3or  6770  nntri2  6771  nntri1  6773  nnsseleq  6778  diffisn  7201  fival  7309  djulclb  7401  exmidomniim  7487  exmidomni  7488  omniwomnimkv  7513  nninfwlpoimlemginf  7522  exmidontriimlem1  7583  3nsssucpw1  7601  addnqprlemfu  7933  mulnqprlemfu  7949  addcanprlemu  7988  cauappcvgprlemladdru  8029  apreap  8923  mulap0r  8951  mul0eqap  9008  nnm1nn0  9615  elnn0z  9668  zleloe  9702  nneoor  9759  nneo  9760  zeo2  9763  uzm1  9969  nn01to3  10033  uzsplit  10516  fzospliti  10602  fzouzsplit  10605  qavgle  10710  xrmaxiflemlub  12039  fz1f1o  12166  fprodsplitdc  12388  fprodcl2lem  12397  ef0lem  12452  zeo3  12660  bezoutlemmain  12800  nninfctlemfo  12842  prmdc  12933  unennn  13346  exmidunben  13375  fnpr2ob  13720  ivthdichlem  15877  plycoeid3  15983  lgsval  16328  lgsfvalg  16329  lgsdilem  16351  wexmiddiffilem  17248  wexmiddifxylem  17250  idjudju  17252  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264  nninfnfiinf  17272  exmidsbthrlem  17273  sbthomlem  17276  trilpolemeq1  17296