Theorem orcomd 885

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

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

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 862

This theorem is used by:  olcd  888  orcnd  892  19.33b  1917  elunnel2  4154  swopo  5569  fr2nr  5627  ordtri1  6396  ordequn  6468  ssonprc  7801  ordunpr  7837  ordunisuc2  7855  2oconcl  8511  erdisj  8775  ordtypelem7  9518  ackbij1lem18  10314  fin23lem19  10414  gchi  10709  inar1  10860  inatsk  10863  avgle  12588  nnm1nn0  12647  zle0orge1  12710  uzsplit  13730  fzospliti  13826  fzouzsplit  13829  znsqcld  14305  fz1f1o  15876  fnpr2ob  17730  odcl  19750  gexcl  19794  lssvs0or  21388  lspdisj  21403  lspsncv0  21424  mdetralt  22923  filconn  24202  limccnp  26211  dgrlt  26585  logreclem  27090  atans2  27259  basellem3  27410  sqff1o  27509  nosep2o  28039  elnns2  28727  nnm1n0s  28761  zcuts0  28794  n0seo  28807  tgcgrsub2  29058  legov3  29061  tghlsub  29086  colline  29118  tglowdim2ln  29120  mirbtwnhl  29152  colmid  29160  symquadlem  29161  midexlem  29164  ragperp  29192  colperp  29205  midex  29213  oppperpex  29229  hlpasch  29234  colopp  29247  plngcplem  29263  plngmiropp  29272  lmieu  29289  lmicom  29293  lmimid  29299  lmiisolem  29301  trgcopy  29311  cgracgr  29325  cgraswap  29327  cgracol  29336  hashecclwwlkn1  30668  xlt2addrd  33393  fprodex01  33458  ssmxidl  34041  drngmxidlr  34044  dflring3  34071  lvecdim0  34281  minplyirred  34385  irredminply  34390  zarclssn  34547  esumcvgre  34765  ordtoplem  37265  ordcmp  37277  onsucuni3  38333  dvasin  38665  eqvreldisj  39673  lkrshp4  40208  2at0mat0  40625  trlator0  41271  dia2dimlem2  42165  dia2dimlem3  42166  dochkrshp  42486  dochkrshp4  42489  lcfl6  42600  lclkrlem2k  42617  hdmap14lem6  42973  hgmapval0  42992  sticksstones12a  43250  sticksstones13  43252  acongneg2  44027  unxpwdom3  44140  dflim5  44374  mnuprdlem1  45299  mnurndlem1  45308  disjinfi  46250  xrssre  46403  icccncfext  46940  wallispilem3  47120  fourierdlem93  47252  fourierdlem101  47260  grlimprclnbgrvtx  49140  gpg5nbgrvtx13starlem3  49214  nneop  49681  itsclinecirc0  49928  itsclinecirc0b  49929  itsclinecirc0in  49930  inlinecirc02plem  49941  inlinecirc02p  49942