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  1920  elunnel2  4157  swopo  5574  fr2nr  5632  ordtri1  6414  ordequn  6486  ssonprc  7825  ordunpr  7861  ordunisuc2  7879  2oconcl  8539  erdisj  8803  ordtypelem7  9545  ackbij1lem18  10341  fin23lem19  10441  gchi  10736  inar1  10887  inatsk  10890  avgle  12615  nnm1nn0  12674  zle0orge1  12737  uzsplit  13757  fzospliti  13853  fzouzsplit  13856  znsqcld  14332  fz1f1o  15905  fnpr2ob  17759  odcl  19780  gexcl  19824  lssvs0or  21418  lspdisj  21433  lspsncv0  21454  mdetralt  22953  filconn  24232  limccnp  26241  dgrlt  26615  logreclem  27120  atans2  27289  basellem3  27440  sqff1o  27539  nosep2o  28069  elnns2  28757  nnm1n0s  28791  zcuts0  28824  n0seo  28837  tgcgrsub2  29088  legov3  29091  tghlsub  29116  colline  29148  tglowdim2ln  29150  mirbtwnhl  29182  colmid  29190  symquadlem  29191  midexlem  29194  ragperp  29222  colperp  29235  midex  29243  oppperpex  29259  hlpasch  29264  colopp  29277  plngcplem  29293  plngmiropp  29302  lmieu  29319  lmicom  29323  lmimid  29329  lmiisolem  29331  trgcopy  29341  cgracgr  29355  cgraswap  29357  cgracol  29366  hashecclwwlkn1  30698  xlt2addrd  33421  fprodex01  33486  ssmxidl  34069  drngmxidlr  34072  dflring3  34099  lvecdim0  34309  minplyirred  34413  irredminply  34418  zarclssn  34575  esumcvgre  34793  ordtoplem  37401  ordcmp  37413  onsucuni3  38482  dvasin  38814  eqvreldisj  39822  lkrshp4  40357  2at0mat0  40774  trlator0  41420  dia2dimlem2  42314  dia2dimlem3  42315  dochkrshp  42635  dochkrshp4  42638  lcfl6  42749  lclkrlem2k  42766  hdmap14lem6  43122  hgmapval0  43141  sticksstones12a  43399  sticksstones13  43401  acongneg2  44177  unxpwdom3  44290  dflim5  44523  mnuprdlem1  45448  mnurndlem1  45457  disjinfi  46412  xrssre  46565  icccncfext  47102  wallispilem3  47282  fourierdlem93  47414  fourierdlem101  47422  grlimprclnbgrvtx  49302  gpg5nbgrvtx13starlem3  49376  nneop  49843  itsclinecirc0  50090  itsclinecirc0b  50091  itsclinecirc0in  50092  inlinecirc02plem  50103  inlinecirc02p  50104