Theorem orcomd 388

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

Syntax hints:   -> wi 4   \/ wo 368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370

This theorem is referenced by:  olcd  393  19.33b  1668  swopo  4805  fr2nr  4852  ordtri1  4906  ssonprc  6600  ordunpr  6634  ordunisuc2  6652  2oconcl  7145  erdisj  7351  ordtypelem7  7940  ackbij1lem18  8608  fin23lem19  8707  gchi  8993  inar1  9144  inatsk  9147  avgle  10771  nnm1nn0  10828  uzsplit  11741  fzm1  11749  fzospliti  11816  fzouzsplit  11819  fz1f1o  13483  odcl  16351  gexcl  16391  lssvs0or  17534  lspdisj  17549  lspsncv0  17570  mdetralt  18872  filcon  20114  limccnp  22025  dgrlt  22392  logreclem  22873  atans2  22985  basellem3  23079  sqff1o  23179  legov3  23706  coltr2  23736  colline  23738  tglowdim2ln  23740  colmid  23768  symquadlem  23769  krippenlem  23770  midexlem  23772  ragperp  23797  colperp  23803  mideu  23809  lmieu  23822  lmicom  23826  lmimid  23831  lmiisolem  23833  hashecclwwlkn1  24498  xlt2addrd  27234  eulerpartlemgvv  27943  nobndup  29025  ordtoplem  29465  ordcmp  29477  dvasin  29669  unitresr  30075  acongneg2  30508  unxpwdom3  30636  icccncfext  31183  wallispilem3  31324  fourierdlem93  31457  fourierdlem101  31465  lkrshp4  33782  2at0mat0  34198  trlator0  34844  dia2dimlem2  35739  dia2dimlem3  35740  dochkrshp  36060  dochkrshp4  36063  lcfl6  36174  lclkrlem2k  36191  hdmap14lem6  36550  hgmapval0  36569