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  1664  swopo  4751  fr2nr  4798  ordtri1  4852  ssonprc  6505  ordunpr  6539  ordunisuc2  6557  2oconcl  7045  erdisj  7250  ordtypelem7  7841  ackbij1lem18  8509  fin23lem19  8608  gchi  8894  inar1  9045  inatsk  9048  avgle  10669  nnm1nn0  10724  uzsplit  11633  fzm1  11643  fzospliti  11684  fzouzsplit  11687  fz1f1o  13291  odcl  16145  gexcl  16185  lssvs0or  17299  lspdisj  17314  lspsncv0  17335  mdetralt  18532  filcon  19574  limccnp  21484  dgrlt  21851  logreclem  22332  atans2  22444  basellem3  22538  sqff1o  22638  coltr2  23177  colline  23179  tglowdim2ln  23181  colmid  23210  symquadlem  23211  krippenlem  23212  midexlem  23214  ragperp  23238  mideu  23247  xlt2addrd  26187  eulerpartlemgvv  26895  nobndup  27977  ordtoplem  28417  ordcmp  28429  dvasin  28620  unitresr  29026  acongneg2  29460  unxpwdom3  29588  wallispilem3  30002  hashecclwwlkn1  30648  lkrshp4  33061  2at0mat0  33477  trlator0  34123  dia2dimlem2  35018  dia2dimlem3  35019  dochkrshp  35339  dochkrshp4  35342  lcfl6  35453  lclkrlem2k  35470  hdmap14lem6  35829  hgmapval0  35848