Theorem orcomd 389

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

Syntax hints:   -> wi 4   \/ wo 369

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 188  df-or 371

This theorem is referenced by:  olcd  394  19.33b  1742  swopo  4784  fr2nr  4831  ordtri1  5475  ssonprc  6633  ordunpr  6667  ordunisuc2  6685  2oconcl  7216  erdisj  7422  ordtypelem7  8048  ackbij1lem18  8674  fin23lem19  8773  gchi  9056  inar1  9207  inatsk  9210  avgle  10861  nnm1nn0  10918  uzsplit  11873  fzospliti  11957  fzouzsplit  11960  fz1f1o  13775  odcl  17184  odclOLD  17200  gexcl  17230  lssvs0or  18332  lspdisj  18347  lspsncv0  18368  mdetralt  19631  filcon  20896  limccnp  22844  dgrlt  23218  logreclem  23697  atans2  23855  basellem3  24007  sqff1o  24107  tgcgrsub2  24638  legov3  24641  colline  24692  tglowdim2ln  24694  mirbtwnhl  24723  colmid  24731  symquadlem  24732  midexlem  24735  ragperp  24760  colperp  24769  midex  24777  oppperpex  24793  hlpasch  24796  colopp  24809  colhp  24810  lmieu  24824  lmicom  24828  lmimid  24834  lmiisolem  24836  trgcopy  24844  cgracgr  24858  cgraswap  24860  cgracol  24867  hashecclwwlkn1  25560  znsqcld  28329  xlt2addrd  28344  esumcvgre  28920  eulerpartlemgvv  29217  nobndup  30594  ordtoplem  31100  ordcmp  31112  onsucuni3  31734  dvasin  31992  unitresr  32283  lkrshp4  32643  2at0mat0  33059  trlator0  33706  dia2dimlem2  34602  dia2dimlem3  34603  dochkrshp  34923  dochkrshp4  34926  lcfl6  35037  lclkrlem2k  35054  hdmap14lem6  35413  hgmapval0  35432  acongneg2  35797  unxpwdom3  35923  elunnel2  37333  disjinfi  37429  xrssre  37525  icccncfext  37705  wallispilem3  37869  fourierdlem93  38003  fourierdlem101  38011  nneop  39954