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

Theorem orcomd 402
 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 401 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 208 1 (𝜑 → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382 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 384 This theorem is referenced by:  olcd  407  19.33b  1950  swopo  5185  fr2nr  5232  ordtri1  5905  ordequn  5977  ssonprc  7145  ordunpr  7179  ordunisuc2  7197  2oconcl  7740  erdisj  7949  ordtypelem7  8582  ackbij1lem18  9222  fin23lem19  9321  gchi  9609  inar1  9760  inatsk  9763  avgle  11437  nnm1nn0  11497  uzsplit  12576  fzospliti  12665  fzouzsplit  12668  fz1f1o  14611  odcl  18126  gexcl  18166  lssvs0or  19283  lspdisj  19298  lspsncv0  19319  mdetralt  20587  filconn  21859  limccnp  23825  dgrlt  24192  logreclem  24670  atans2  24828  basellem3  24979  sqff1o  25078  tgcgrsub2  25660  legov3  25663  colline  25714  tglowdim2ln  25716  mirbtwnhl  25745  colmid  25753  symquadlem  25754  midexlem  25757  ragperp  25782  colperp  25791  midex  25799  oppperpex  25815  hlpasch  25818  colopp  25831  colhp  25832  lmieu  25846  lmicom  25850  lmimid  25856  lmiisolem  25858  trgcopy  25866  cgracgr  25880  cgraswap  25882  cgracol  25889  hashecclwwlkn1  27179  znsqcld  29792  xlt2addrd  29803  fprodex01  29851  esumcvgre  30433  eulerpartlemgvv  30718  ordtoplem  32711  ordcmp  32723  onsucuni3  33497  dvasin  33778  unitresr  34167  lkrshp4  34867  2at0mat0  35283  trlator0  35930  dia2dimlem2  36825  dia2dimlem3  36826  dochkrshp  37146  dochkrshp4  37149  lcfl6  37260  lclkrlem2k  37277  hdmap14lem6  37636  hgmapval0  37655  acongneg2  38015  unxpwdom3  38136  elunnel2  39666  disjinfi  39848  xrssre  40031  icccncfext  40572  wallispilem3  40756  fourierdlem93  40888  fourierdlem101  40896  nneop  42799
 Copyright terms: Public domain W3C validator