Theorem orcomd 870

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  olcd  873  orcnd  877  19.33b  1881  r19.30OLD  3116  elunnel2  4146  swopo  5595  fr2nr  5650  ordtri1  6396  ordequn  6466  ssonprc  7784  ordunpr  7823  ordunisuc2  7842  2oconcl  8517  erdisj  8771  ordtypelem7  9539  ackbij1lem18  10252  fin23lem19  10351  gchi  10639  inar1  10790  inatsk  10793  avgle  12476  nnm1nn0  12535  zle0orge1  12597  uzsplit  13597  fzospliti  13688  fzouzsplit  13691  znsqcld  14150  fz1f1o  15680  fnpr2ob  17531  odcl  19482  gexcl  19526  lssvs0or  20987  lspdisj  21002  lspsncv0  21023  mdetralt  22497  filconn  23774  limccnp  25807  dgrlt  26188  logreclem  26681  atans2  26850  basellem3  27002  sqff1o  27101  nosep2o  27602  elnns2  28196  tgcgrsub2  28386  legov3  28389  colline  28440  tglowdim2ln  28442  mirbtwnhl  28471  colmid  28479  symquadlem  28480  midexlem  28483  ragperp  28508  colperp  28520  midex  28528  oppperpex  28544  hlpasch  28547  colopp  28560  lmieu  28575  lmicom  28579  lmimid  28585  lmiisolem  28587  trgcopy  28595  cgracgr  28609  cgraswap  28611  cgracol  28619  hashecclwwlkn1  29874  xlt2addrd  32512  fprodex01  32570  ssmxidl  33123  lvecdim0  33236  minplyirred  33317  irredminply  33320  zarclssn  33410  esumcvgre  33646  ordtoplem  35855  ordcmp  35867  onsucuni3  36782  dvasin  37112  eqvreldisj  38023  lkrshp4  38517  2at0mat0  38935  trlator0  39581  dia2dimlem2  40475  dia2dimlem3  40476  dochkrshp  40796  dochkrshp4  40799  lcfl6  40910  lclkrlem2k  40927  hdmap14lem6  41283  hgmapval0  41302  sticksstones12a  41561  sticksstones13  41563  acongneg2  42320  unxpwdom3  42441  dflim5  42681  mnuprdlem1  43632  mnurndlem1  43641  disjinfi  44488  xrssre  44653  icccncfext  45198  wallispilem3  45378  fourierdlem93  45510  fourierdlem101  45518  nneop  47522  itsclinecirc0  47769  itsclinecirc0b  47770  itsclinecirc0in  47771  inlinecirc02plem  47782  inlinecirc02p  47783