Theorem orcomd 394

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

Syntax hints:   -> wi 4   \/ wo 374

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 190  df-or 376

This theorem is referenced by:  olcd  399  19.33b  1752  swopo  4743  fr2nr  4790  ordtri1  5435  ssonprc  6607  ordunpr  6641  ordunisuc2  6659  2oconcl  7192  erdisj  7398  ordtypelem7  8026  ackbij1lem18  8654  fin23lem19  8753  gchi  9036  inar1  9187  inatsk  9190  avgle  10844  nnm1nn0  10901  uzsplit  11857  fzospliti  11943  fzouzsplit  11946  fz1f1o  13787  odcl  17196  odclOLD  17212  gexcl  17242  lssvs0or  18344  lspdisj  18359  lspsncv0  18380  mdetralt  19644  filcon  20909  limccnp  22858  dgrlt  23232  logreclem  23711  atans2  23869  basellem3  24021  sqff1o  24121  tgcgrsub2  24652  legov3  24655  colline  24706  tglowdim2ln  24708  mirbtwnhl  24737  colmid  24745  symquadlem  24746  midexlem  24749  ragperp  24774  colperp  24783  midex  24791  oppperpex  24807  hlpasch  24810  colopp  24823  colhp  24824  lmieu  24838  lmicom  24842  lmimid  24848  lmiisolem  24850  trgcopy  24858  cgracgr  24872  cgraswap  24874  cgracol  24881  hashecclwwlkn1  25574  znsqcld  28331  xlt2addrd  28346  esumcvgre  28919  eulerpartlemgvv  29215  nobndup  30595  ordtoplem  31101  ordcmp  31113  onsucuni3  31772  dvasin  32030  unitresr  32321  lkrshp4  32676  2at0mat0  33092  trlator0  33739  dia2dimlem2  34635  dia2dimlem3  34636  dochkrshp  34956  dochkrshp4  34959  lcfl6  35070  lclkrlem2k  35087  hdmap14lem6  35446  hgmapval0  35465  acongneg2  35829  unxpwdom3  35955  elunnel2  37357  disjinfi  37478  xrssre  37602  icccncfext  37807  wallispilem3  37986  fourierdlem93  38120  fourierdlem101  38128  nneop  40658