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

Theorem orcomd 403
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 402 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 208 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  olcd  408  19.33b  1810  swopo  5005  fr2nr  5052  ordtri1  5715  ordequn  5787  ssonprc  6939  ordunpr  6973  ordunisuc2  6991  2oconcl  7528  erdisj  7739  ordtypelem7  8373  ackbij1lem18  9003  fin23lem19  9102  gchi  9390  inar1  9541  inatsk  9544  avgle  11218  nnm1nn0  11278  uzsplit  12353  fzospliti  12441  fzouzsplit  12444  fz1f1o  14374  odcl  17876  gexcl  17916  lssvs0or  19029  lspdisj  19044  lspsncv0  19065  mdetralt  20333  filconn  21597  limccnp  23561  dgrlt  23926  logreclem  24400  atans2  24558  basellem3  24709  sqff1o  24808  tgcgrsub2  25390  legov3  25393  colline  25444  tglowdim2ln  25446  mirbtwnhl  25475  colmid  25483  symquadlem  25484  midexlem  25487  ragperp  25512  colperp  25521  midex  25529  oppperpex  25545  hlpasch  25548  colopp  25561  colhp  25562  lmieu  25576  lmicom  25580  lmimid  25586  lmiisolem  25588  trgcopy  25596  cgracgr  25610  cgraswap  25612  cgracol  25619  hashecclwwlksn1  26820  znsqcld  29352  xlt2addrd  29364  esumcvgre  29931  eulerpartlemgvv  30216  nobndup  31560  nosino  31572  ordtoplem  32073  ordcmp  32085  onsucuni3  32844  dvasin  33125  unitresr  33514  lkrshp4  33872  2at0mat0  34288  trlator0  34935  dia2dimlem2  35831  dia2dimlem3  35832  dochkrshp  36152  dochkrshp4  36155  lcfl6  36266  lclkrlem2k  36283  hdmap14lem6  36642  hgmapval0  36661  acongneg2  37021  unxpwdom3  37142  elunnel2  38678  disjinfi  38851  xrssre  39025  icccncfext  39401  wallispilem3  39588  fourierdlem93  39720  fourierdlem101  39728  nneop  41605
  Copyright terms: Public domain W3C validator