Theorem orcomd 386

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

Syntax hints:   -> wi 4   \/ wo 366

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 368

This theorem is referenced by:  olcd  391  19.33b  1717  swopo  4753  fr2nr  4800  ordtri1  5442  ssonprc  6609  ordunpr  6643  ordunisuc2  6661  2oconcl  7189  erdisj  7395  ordtypelem7  7982  ackbij1lem18  8648  fin23lem19  8747  gchi  9031  inar1  9182  inatsk  9185  avgle  10820  nnm1nn0  10877  uzsplit  11803  fzospliti  11887  fzouzsplit  11890  fz1f1o  13679  odcl  16882  gexcl  16922  lssvs0or  18074  lspdisj  18089  lspsncv0  18110  mdetralt  19400  filcon  20674  limccnp  22585  dgrlt  22953  logreclem  23427  atans2  23585  basellem3  23735  sqff1o  23835  tgcgrsub2  24363  legov3  24366  coltr2  24411  colline  24413  tglowdim2ln  24415  mirbtwnhl  24443  colmid  24448  symquadlem  24449  midexlem  24452  ragperp  24477  colperp  24486  midex  24494  lmieu  24533  lmicom  24537  lmimid  24542  lmiisolem  24544  cgracgr  24560  cgraswap  24562  hashecclwwlkn1  25238  znsqcld  27994  xlt2addrd  28006  esumcvgre  28524  eulerpartlemgvv  28807  nobndup  30147  ordtoplem  30654  ordcmp  30666  dvasin  31454  unitresr  31745  lkrshp4  32106  2at0mat0  32522  trlator0  33169  dia2dimlem2  34065  dia2dimlem3  34066  dochkrshp  34386  dochkrshp4  34389  lcfl6  34500  lclkrlem2k  34517  hdmap14lem6  34876  hgmapval0  34895  acongneg2  35256  unxpwdom3  35383  elunnel2  36775  icccncfext  37039  wallispilem3  37198  fourierdlem93  37331  fourierdlem101  37339  nneop  38634