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

Theorem orcomd 388
Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)
Hypothesis
Ref Expression
orcomd.1
Assertion
Ref Expression
orcomd

Proof of Theorem orcomd
StepHypRef Expression
1 orcomd.1 . 2
2 orcom 387 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  olcd  393  19.33b  1696  swopo  4815  fr2nr  4862  ordtri1  4916  ssonprc  6627  ordunpr  6661  ordunisuc2  6679  2oconcl  7172  erdisj  7378  ordtypelem7  7970  ackbij1lem18  8638  fin23lem19  8737  gchi  9023  inar1  9174  inatsk  9177  avgle  10805  nnm1nn0  10862  uzsplit  11779  fzospliti  11857  fzouzsplit  11860  fz1f1o  13532  odcl  16560  gexcl  16600  lssvs0or  17756  lspdisj  17771  lspsncv0  17792  mdetralt  19110  filcon  20384  limccnp  22295  dgrlt  22663  logreclem  23150  atans2  23262  basellem3  23356  sqff1o  23456  legov3  23984  coltr2  24028  colline  24030  tglowdim2ln  24032  mirbtwnhl  24060  colmid  24065  symquadlem  24066  midexlem  24069  ragperp  24094  colperp  24103  midex  24111  lmieu  24150  lmicom  24154  lmimid  24159  lmiisolem  24161  hashecclwwlkn1  24834  znsqcld  27561  xlt2addrd  27578  eulerpartlemgvv  28315  nobndup  29460  ordtoplem  29900  ordcmp  29912  dvasin  30103  unitresr  30483  acongneg2  30915  unxpwdom3  31041  elunnel2  31415  icccncfext  31690  wallispilem3  31849  fourierdlem93  31982  fourierdlem101  31990  lkrshp4  34833  2at0mat0  35249  trlator0  35896  dia2dimlem2  36792  dia2dimlem3  36793  dochkrshp  37113  dochkrshp4  37116  lcfl6  37227  lclkrlem2k  37244  hdmap14lem6  37603  hgmapval0  37622
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
  Copyright terms: Public domain W3C validator