Theorem orcomd 719

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

Syntax hints:   -> wi 4   \/ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  olcd  724  stdcndcOLD  832  pm5.54dc  904  r19.30dc  2604  exmid1dc  4160  swopo  4265  sotritrieq  4284  ontriexmidim  4479  ontri2orexmidim  4529  reg3exmidlemwe  4536  acexmidlemcase  5813  2oconcl  6380  nntri3or  6433  nntri2  6434  nntri1  6436  nnsseleq  6441  diffisn  6831  fival  6907  djulclb  6989  exmidomniim  7067  exmidomni  7068  omniwomnimkv  7093  exmidontriimlem1  7139  3nsssucpw1  7154  addnqprlemfu  7463  mulnqprlemfu  7479  addcanprlemu  7518  cauappcvgprlemladdru  7559  apreap  8445  mulap0r  8473  mul0eqap  8527  nnm1nn0  9114  elnn0z  9163  zleloe  9197  nneoor  9249  nneo  9250  zeo2  9253  uzm1  9452  nn01to3  9508  uzsplit  9976  fzospliti  10057  fzouzsplit  10060  qavgle  10140  xrmaxiflemlub  11127  fz1f1o  11254  fprodsplitdc  11475  fprodcl2lem  11484  ef0lem  11539  zeo3  11740  bezoutlemmain  11862  unennn  12098  exmidunben  12127  nninfalllem1  13543  nninfall  13544  nninfsellemqall  13550  exmidsbthrlem  13556  sbthomlem  13559  trilpolemeq1  13574