MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcomd Unicode version

Theorem orcomd 377
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
StepHypRef Expression
1 orcomd.1 . 2  |-  ( ph  ->  ( ps  \/  ch ) )
2 orcom 376 . 2  |-  ( ( ps  \/  ch )  <->  ( ch  \/  ps )
)
31, 2sylib 188 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  olcd  382  19.33b  1598  swopo  4340  fr2nr  4387  ordtri1  4441  ssonprc  4599  ordunpr  4633  ordunisuc2  4651  2oconcl  6518  erdisj  6723  ordtypelem7  7255  ackbij1lem18  7879  fin23lem19  7978  gchi  8262  inar1  8413  inatsk  8416  avgle  9969  nnm1nn0  10021  uzsplit  10871  fzm1  10878  fzospliti  10914  fzouzsplit  10917  fz1f1o  12199  odcl  14867  gexcl  14907  lssvs0or  15879  lspdisj  15894  lspsncv0  15915  filcon  17594  limccnp  19257  dgrlt  19663  logreclem  20132  atans2  20243  basellem3  20336  sqff1o  20436  xlt2addrd  23268  nobndup  24425  ordtoplem  24946  ordcmp  24958  dvreasin  25026  acongneg2  27167  unxpwdom3  27359  wallispilem3  27919  lkrshp4  29920  2at0mat0  30336  trlator0  30982  dia2dimlem2  31877  dia2dimlem3  31878  dochkrshp  32198  dochkrshp4  32201  lcfl6  32312  lclkrlem2k  32329  hdmap14lem6  32688  hgmapval0  32707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator