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

Theorem orcomd 865
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 864 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 219 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 841
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 842
This theorem is referenced by:  unitresr  867  olcd  870  19.33b  1877  r19.30  3335  swopo  5477  fr2nr  5526  ordtri1  6217  ordequn  6284  ssonprc  7496  ordunpr  7530  ordunisuc2  7548  2oconcl  8117  erdisj  8330  ordtypelem7  8976  ackbij1lem18  9647  fin23lem19  9746  gchi  10034  inar1  10185  inatsk  10188  avgle  11867  nnm1nn0  11926  zle0orge1  11986  uzsplit  12967  fzospliti  13057  fzouzsplit  13060  znsqcld  13514  fz1f1o  15055  fnpr2ob  16819  odcl  18593  gexcl  18634  lssvs0or  19811  lspdisj  19826  lspsncv0  19847  mdetralt  21145  filconn  22419  limccnp  24416  dgrlt  24783  logreclem  25267  atans2  25436  basellem3  25587  sqff1o  25686  tgcgrsub2  26308  legov3  26311  colline  26362  tglowdim2ln  26364  mirbtwnhl  26393  colmid  26401  symquadlem  26402  midexlem  26405  ragperp  26430  colperp  26442  midex  26450  oppperpex  26466  hlpasch  26469  colopp  26482  lmieu  26497  lmicom  26501  lmimid  26507  lmiisolem  26509  trgcopy  26517  cgracgr  26531  cgraswap  26533  cgracol  26541  hashecclwwlkn1  27783  xlt2addrd  30408  fprodex01  30468  lvecdim0  30904  esumcvgre  31249  ordtoplem  33680  ordcmp  33692  onsucuni3  34530  dvasin  34859  eqvreldisj  35729  lkrshp4  36124  2at0mat0  36541  trlator0  37187  dia2dimlem2  38081  dia2dimlem3  38082  dochkrshp  38402  dochkrshp4  38405  lcfl6  38516  lclkrlem2k  38533  hdmap14lem6  38889  hgmapval0  38908  acongneg2  39452  unxpwdom3  39573  mnuprdlem1  40485  mnurndlem1  40494  elunnel2  41173  disjinfi  41330  xrssre  41492  icccncfext  42046  wallispilem3  42229  fourierdlem93  42361  fourierdlem101  42369  nneop  44514  itsclinecirc0  44688  itsclinecirc0b  44689  itsclinecirc0in  44690  inlinecirc02plem  44701  inlinecirc02p  44702
  Copyright terms: Public domain W3C validator