Theorem orcomd 737

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

Syntax hints:   -> wi 4   \/ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  olcd  742  stdcndcOLD  854  pm5.54dc  926  r19.30dc  2681  exmid1dc  4296  swopo  4409  sotritrieq  4428  ontriexmidim  4626  ontri2orexmidim  4676  reg3exmidlemwe  4683  acexmidlemcase  6023  2oconcl  6650  nntri3or  6704  nntri2  6705  nntri1  6707  nnsseleq  6712  diffisn  7125  fival  7212  djulclb  7297  exmidomniim  7383  exmidomni  7384  omniwomnimkv  7409  nninfwlpoimlemginf  7418  exmidontriimlem1  7479  3nsssucpw1  7497  addnqprlemfu  7823  mulnqprlemfu  7839  addcanprlemu  7878  cauappcvgprlemladdru  7919  apreap  8809  mulap0r  8837  mul0eqap  8892  nnm1nn0  9485  elnn0z  9536  zleloe  9570  nneoor  9626  nneo  9627  zeo2  9630  uzm1  9831  nn01to3  9895  uzsplit  10372  fzospliti  10458  fzouzsplit  10461  qavgle  10564  xrmaxiflemlub  11871  fz1f1o  11998  fprodsplitdc  12220  fprodcl2lem  12229  ef0lem  12284  zeo3  12492  bezoutlemmain  12632  nninfctlemfo  12674  prmdc  12765  unennn  13081  exmidunben  13110  fnpr2ob  13486  ivthdichlem  15445  plycoeid3  15551  lgsval  15806  lgsfvalg  15807  lgsdilem  15829  nninfalllem1  16717  nninfall  16718  nninfsellemqall  16724  nninfnfiinf  16732  exmidsbthrlem  16733  sbthomlem  16736  trilpolemeq1  16755