Theorem orcomd 882

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

Step	Hyp	Ref	Expression
1		orcomd.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		orcom 881	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	1, 2	sylib 220	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  olcd  885  orcnd  889  19.33b  1906  elunnel2  4109  swopo  5567  fr2nr  5625  ordtri1  6379  ordequn  6451  ssonprc  7770  ordunpr  7806  ordunisuc2  7824  2oconcl  8472  erdisj  8736  ordtypelem7  9470  ackbij1lem18  10203  fin23lem19  10304  gchi  10593  inar1  10744  inatsk  10747  avgle  12473  nnm1nn0  12532  zle0orge1  12595  uzsplit  13611  fzospliti  13707  fzouzsplit  13710  znsqcld  14185  fz1f1o  15747  fnpr2ob  17598  odcl  19586  gexcl  19630  lssvs0or  21187  lspdisj  21202  lspsncv0  21223  mdetralt  22675  filconn  23950  limccnp  25960  dgrlt  26333  logreclem  26834  atans2  27003  basellem3  27154  sqff1o  27253  nosep2o  27753  elnns2  28441  nnm1n0s  28475  zcuts0  28508  n0seo  28521  tgcgrsub2  28771  legov3  28774  colline  28826  tglowdim2ln  28828  mirbtwnhl  28860  colmid  28868  symquadlem  28869  midexlem  28872  ragperp  28897  colperp  28909  midex  28917  oppperpex  28933  hlpasch  28936  colopp  28949  lmieu  28964  lmicom  28968  lmimid  28974  lmiisolem  28976  trgcopy  28984  plngcplem  28999  cgracgr  29019  cgraswap  29021  cgracol  29029  hashecclwwlkn1  30286  xlt2addrd  32967  fprodex01  33033  ssmxidl  33665  drngmxidlr  33669  dflring3  33696  lvecdim0  33906  minplyirred  34010  irredminply  34015  zarclssn  34172  esumcvgre  34390  ordtoplem  36800  ordcmp  36812  onsucuni3  37866  dvasin  38208  eqvreldisj  39202  lkrshp4  39737  2at0mat0  40154  trlator0  40800  dia2dimlem2  41694  dia2dimlem3  41695  dochkrshp  42015  dochkrshp4  42018  lcfl6  42129  lclkrlem2k  42146  hdmap14lem6  42502  hgmapval0  42521  sticksstones12a  42779  sticksstones13  42781  acongneg2  43559  unxpwdom3  43677  dflim5  43911  mnuprdlem1  44839  mnurndlem1  44848  disjinfi  45761  xrssre  45915  icccncfext  46452  wallispilem3  46632  fourierdlem93  46764  fourierdlem101  46772  grlimprclnbgrvtx  48612  gpg5nbgrvtx13starlem3  48686  nneop  49139  itsclinecirc0  49386  itsclinecirc0b  49387  itsclinecirc0in  49388  inlinecirc02plem  49399  inlinecirc02p  49400