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  1595  swopo  4324  fr2nr  4371  ordtri1  4425  ssonprc  4583  ordunpr  4617  ordunisuc2  4635  2oconcl  6502  erdisj  6707  ordtypelem7  7239  ackbij1lem18  7863  fin23lem19  7962  gchi  8246  inar1  8397  inatsk  8400  avgle  9953  nnm1nn0  10005  uzsplit  10855  fzm1  10862  fzospliti  10898  fzouzsplit  10901  fz1f1o  12183  odcl  14851  gexcl  14891  lssvs0or  15863  lspdisj  15878  lspsncv0  15899  filcon  17578  limccnp  19241  dgrlt  19647  logreclem  20116  atans2  20227  basellem3  20320  sqff1o  20420  xlt2addrd  23253  nobndup  24354  ordtoplem  24874  ordcmp  24886  dvreasin  24923  acongneg2  27064  unxpwdom3  27256  wallispilem3  27816  lkrshp4  29298  2at0mat0  29714  trlator0  30360  dia2dimlem2  31255  dia2dimlem3  31256  dochkrshp  31576  dochkrshp4  31579  lcfl6  31690  lclkrlem2k  31707  hdmap14lem6  32066  hgmapval0  32085
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