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

Theorem orcomd 870
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 869 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 217 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 206  df-or 847
This theorem is referenced by:  olcd  873  orcnd  878  19.33b  1889  r19.30OLD  3123  elunnel2  4109  swopo  5555  fr2nr  5610  ordtri1  6349  ordequn  6419  ssonprc  7715  ordunpr  7754  ordunisuc2  7773  2oconcl  8442  erdisj  8659  ordtypelem7  9419  ackbij1lem18  10132  fin23lem19  10231  gchi  10519  inar1  10670  inatsk  10673  avgle  12354  nnm1nn0  12413  zle0orge1  12475  uzsplit  13468  fzospliti  13559  fzouzsplit  13562  znsqcld  14020  fz1f1o  15555  fnpr2ob  17400  odcl  19277  gexcl  19321  lssvs0or  20524  lspdisj  20539  lspsncv0  20560  mdetralt  21909  filconn  23186  limccnp  25207  dgrlt  25579  logreclem  26064  atans2  26233  basellem3  26384  sqff1o  26483  nosep2o  26982  tgcgrsub2  27366  legov3  27369  colline  27420  tglowdim2ln  27422  mirbtwnhl  27451  colmid  27459  symquadlem  27460  midexlem  27463  ragperp  27488  colperp  27500  midex  27508  oppperpex  27524  hlpasch  27527  colopp  27540  lmieu  27555  lmicom  27559  lmimid  27565  lmiisolem  27567  trgcopy  27575  cgracgr  27589  cgraswap  27591  cgracol  27599  hashecclwwlkn1  28850  xlt2addrd  31488  fprodex01  31546  ssmxidl  32059  lvecdim0  32118  zarclssn  32258  esumcvgre  32494  ordtoplem  34839  ordcmp  34851  onsucuni3  35770  dvasin  36094  eqvreldisj  37008  lkrshp4  37502  2at0mat0  37920  trlator0  38566  dia2dimlem2  39460  dia2dimlem3  39461  dochkrshp  39781  dochkrshp4  39784  lcfl6  39895  lclkrlem2k  39912  hdmap14lem6  40268  hgmapval0  40287  sticksstones12a  40497  sticksstones13  40499  acongneg2  41204  unxpwdom3  41325  dflim5  41564  mnuprdlem1  42457  mnurndlem1  42466  disjinfi  43311  xrssre  43481  icccncfext  44023  wallispilem3  44203  fourierdlem93  44335  fourierdlem101  44343  nneop  46507  itsclinecirc0  46754  itsclinecirc0b  46755  itsclinecirc0in  46756  inlinecirc02plem  46767  inlinecirc02p  46768
  Copyright terms: Public domain W3C validator