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

Theorem orcomd 867
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 866 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 219 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 843
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 208  df-or 844
This theorem is referenced by:  unitresr  869  olcd  872  19.33b  1879  r19.30  3342  swopo  5482  fr2nr  5531  ordtri1  6221  ordequn  6288  ssonprc  7498  ordunpr  7532  ordunisuc2  7550  2oconcl  8122  erdisj  8334  ordtypelem7  8980  ackbij1lem18  9651  fin23lem19  9750  gchi  10038  inar1  10189  inatsk  10192  avgle  11871  nnm1nn0  11930  zle0orge1  11990  uzsplit  12972  fzospliti  13062  fzouzsplit  13065  znsqcld  13519  fz1f1o  15060  fnpr2ob  16824  odcl  18587  gexcl  18628  lssvs0or  19805  lspdisj  19820  lspsncv0  19841  mdetralt  21136  filconn  22410  limccnp  24407  dgrlt  24774  logreclem  25256  atans2  25425  basellem3  25577  sqff1o  25676  tgcgrsub2  26298  legov3  26301  colline  26352  tglowdim2ln  26354  mirbtwnhl  26383  colmid  26391  symquadlem  26392  midexlem  26395  ragperp  26420  colperp  26432  midex  26440  oppperpex  26456  hlpasch  26459  colopp  26472  lmieu  26487  lmicom  26491  lmimid  26497  lmiisolem  26499  trgcopy  26507  cgracgr  26521  cgraswap  26523  cgracol  26531  hashecclwwlkn1  27773  xlt2addrd  30398  fprodex01  30458  lvecdim0  30894  esumcvgre  31239  ordtoplem  33670  ordcmp  33682  onsucuni3  34520  dvasin  34848  eqvreldisj  35719  lkrshp4  36114  2at0mat0  36531  trlator0  37177  dia2dimlem2  38071  dia2dimlem3  38072  dochkrshp  38392  dochkrshp4  38395  lcfl6  38506  lclkrlem2k  38523  hdmap14lem6  38879  hgmapval0  38898  acongneg2  39442  unxpwdom3  39563  mnuprdlem1  40476  mnurndlem1  40485  elunnel2  41164  disjinfi  41322  xrssre  41484  icccncfext  42038  wallispilem3  42221  fourierdlem93  42353  fourierdlem101  42361  nneop  44421  itsclinecirc0  44595  itsclinecirc0b  44596  itsclinecirc0in  44597  inlinecirc02plem  44608  inlinecirc02p  44609
  Copyright terms: Public domain W3C validator