Theorem orcomd 871

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  olcd  874  orcnd  878  19.33b  1885  elunnel2  4121  swopo  5560  fr2nr  5618  ordtri1  6368  ordequn  6440  ssonprc  7766  ordunpr  7804  ordunisuc2  7823  2oconcl  8470  erdisj  8731  ordtypelem7  9484  ackbij1lem18  10196  fin23lem19  10296  gchi  10584  inar1  10735  inatsk  10738  avgle  12431  nnm1nn0  12490  zle0orge1  12553  uzsplit  13564  fzospliti  13659  fzouzsplit  13662  znsqcld  14134  fz1f1o  15683  fnpr2ob  17528  odcl  19473  gexcl  19517  lssvs0or  21027  lspdisj  21042  lspsncv0  21063  mdetralt  22502  filconn  23777  limccnp  25799  dgrlt  26179  logreclem  26679  atans2  26848  basellem3  27000  sqff1o  27099  nosep2o  27601  elnns2  28240  nnm1n0s  28271  n0seo  28314  tgcgrsub2  28529  legov3  28532  colline  28583  tglowdim2ln  28585  mirbtwnhl  28614  colmid  28622  symquadlem  28623  midexlem  28626  ragperp  28651  colperp  28663  midex  28671  oppperpex  28687  hlpasch  28690  colopp  28703  lmieu  28718  lmicom  28722  lmimid  28728  lmiisolem  28730  trgcopy  28738  cgracgr  28752  cgraswap  28754  cgracol  28762  hashecclwwlkn1  30013  xlt2addrd  32689  fprodex01  32757  ssmxidl  33452  drngmxidlr  33456  lvecdim0  33609  minplyirred  33708  irredminply  33713  zarclssn  33870  esumcvgre  34088  ordtoplem  36430  ordcmp  36442  onsucuni3  37362  dvasin  37705  eqvreldisj  38612  lkrshp4  39108  2at0mat0  39526  trlator0  40172  dia2dimlem2  41066  dia2dimlem3  41067  dochkrshp  41387  dochkrshp4  41390  lcfl6  41501  lclkrlem2k  41518  hdmap14lem6  41874  hgmapval0  41893  sticksstones12a  42152  sticksstones13  42154  acongneg2  42973  unxpwdom3  43091  dflim5  43325  mnuprdlem1  44268  mnurndlem1  44277  disjinfi  45193  xrssre  45351  icccncfext  45892  wallispilem3  46072  fourierdlem93  46204  fourierdlem101  46212  gpg5nbgrvtx13starlem3  48068  nneop  48519  itsclinecirc0  48766  itsclinecirc0b  48767  itsclinecirc0in  48768  inlinecirc02plem  48779  inlinecirc02p  48780