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  1683  swopo  4800  fr2nr  4847  ordtri1  4901  ssonprc  6612  ordunpr  6646  ordunisuc2  6664  2oconcl  7155  erdisj  7361  ordtypelem7  7952  ackbij1lem18  8620  fin23lem19  8719  gchi  9005  inar1  9156  inatsk  9159  avgle  10787  nnm1nn0  10844  uzsplit  11761  fzm1  11769  fzospliti  11839  fzouzsplit  11842  fz1f1o  13514  odcl  16539  gexcl  16579  lssvs0or  17735  lspdisj  17750  lspsncv0  17771  mdetralt  19088  filcon  20362  limccnp  22273  dgrlt  22641  logreclem  23128  atans2  23240  basellem3  23334  sqff1o  23434  legov3  23962  coltr2  24006  colline  24008  tglowdim2ln  24010  mirbtwnhl  24038  colmid  24043  symquadlem  24044  midexlem  24047  ragperp  24072  colperp  24081  midex  24089  lmieu  24128  lmicom  24132  lmimid  24137  lmiisolem  24139  hashecclwwlkn1  24812  znsqcld  27539  xlt2addrd  27556  eulerpartlemgvv  28293  nobndup  29436  ordtoplem  29876  ordcmp  29888  dvasin  30079  unitresr  30459  acongneg2  30891  unxpwdom3  31017  elunnel2  31369  icccncfext  31644  wallispilem3  31803  fourierdlem93  31936  fourierdlem101  31944  lkrshp4  34708  2at0mat0  35124  trlator0  35771  dia2dimlem2  36667  dia2dimlem3  36668  dochkrshp  36988  dochkrshp4  36991  lcfl6  37102  lclkrlem2k  37119  hdmap14lem6  37478  hgmapval0  37497