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

Theorem orcomd 379
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 378 . 2  |-  ( ( ps  \/  ch )  <->  ( ch  \/  ps )
)
31, 2sylib 190 1  |-  ( ph  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359
This theorem is referenced by:  olcd  384  19.33b  1619  swopo  4515  fr2nr  4562  ordtri1  4616  ssonprc  4774  ordunpr  4808  ordunisuc2  4826  2oconcl  6749  erdisj  6954  ordtypelem7  7495  ackbij1lem18  8119  fin23lem19  8218  gchi  8501  inar1  8652  inatsk  8655  avgle  10211  nnm1nn0  10263  uzsplit  11120  fzm1  11129  fzospliti  11167  fzouzsplit  11170  fz1f1o  12506  odcl  15176  gexcl  15216  lssvs0or  16184  lspdisj  16199  lspsncv0  16220  filcon  17917  limccnp  19780  dgrlt  20186  logreclem  20662  atans2  20773  basellem3  20867  sqff1o  20967  xlt2addrd  24126  nobndup  25657  ordtoplem  26187  ordcmp  26199  dvreasin  26292  acongneg2  27044  unxpwdom3  27235  wallispilem3  27794  lkrshp4  29968  2at0mat0  30384  trlator0  31030  dia2dimlem2  31925  dia2dimlem3  31926  dochkrshp  32246  dochkrshp4  32249  lcfl6  32360  lclkrlem2k  32377  hdmap14lem6  32736  hgmapval0  32755
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 179  df-or 361
  Copyright terms: Public domain W3C validator