Theorem orcomd 884

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 883	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓))
3	1, 2	sylib 221	1 ⊢ (𝜑 → (𝜒 ∨ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 861

This theorem is used by:  olcd  887  orcnd  891  19.33b  1914  elunnel2  4108  swopo  5579  fr2nr  5637  ordtri1  6394  ordequn  6466  ssonprc  7784  ordunpr  7820  ordunisuc2  7838  2oconcl  8486  erdisj  8750  ordtypelem7  9484  ackbij1lem18  10226  fin23lem19  10326  gchi  10615  inar1  10766  inatsk  10769  avgle  12492  nnm1nn0  12551  zle0orge1  12614  uzsplit  13631  fzospliti  13727  fzouzsplit  13730  znsqcld  14205  fz1f1o  15768  fnpr2ob  17618  odcl  19612  gexcl  19656  lssvs0or  21245  lspdisj  21260  lspsncv0  21281  mdetralt  22776  filconn  24051  limccnp  26061  dgrlt  26434  logreclem  26938  atans2  27107  basellem3  27258  sqff1o  27357  nosep2o  27857  elnns2  28545  nnm1n0s  28579  zcuts0  28612  n0seo  28625  tgcgrsub2  28875  legov3  28878  colline  28934  tglowdim2ln  28936  mirbtwnhl  28968  colmid  28976  symquadlem  28977  midexlem  28980  ragperp  29008  colperp  29021  midex  29029  oppperpex  29045  hlpasch  29049  colopp  29062  plngcplem  29078  plngmiropp  29087  lmieu  29104  lmicom  29108  lmimid  29114  lmiisolem  29116  trgcopy  29126  cgracgr  29140  cgraswap  29142  cgracol  29150  hashecclwwlkn1  30439  xlt2addrd  33115  fprodex01  33180  ssmxidl  33766  drngmxidlr  33769  dflring3  33796  lvecdim0  34006  minplyirred  34110  irredminply  34115  zarclssn  34272  esumcvgre  34490  ordtoplem  36974  ordcmp  36986  onsucuni3  38041  dvasin  38383  eqvreldisj  39375  lkrshp4  39910  2at0mat0  40327  trlator0  40973  dia2dimlem2  41867  dia2dimlem3  41868  dochkrshp  42188  dochkrshp4  42191  lcfl6  42302  lclkrlem2k  42319  hdmap14lem6  42675  hgmapval0  42694  sticksstones12a  42952  sticksstones13  42954  acongneg2  43732  unxpwdom3  43850  dflim5  44084  mnuprdlem1  45010  mnurndlem1  45019  disjinfi  45938  xrssre  46092  icccncfext  46629  wallispilem3  46809  fourierdlem93  46941  fourierdlem101  46949  grlimprclnbgrvtx  48792  gpg5nbgrvtx13starlem3  48866  nneop  49334  itsclinecirc0  49581  itsclinecirc0b  49582  itsclinecirc0in  49583  inlinecirc02plem  49594  inlinecirc02p  49595