Theorem orcomd 867

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

Syntax hints:   → wi 4   ∨ wo 843

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 844

This theorem is referenced by:  olcd  870  orcnd  875  19.33b  1886  r19.30OLD  3119  elunnel2  4151  swopo  5600  fr2nr  5655  ordtri1  6398  ordequn  6468  ssonprc  7779  ordunpr  7818  ordunisuc2  7837  2oconcl  8507  erdisj  8759  ordtypelem7  9523  ackbij1lem18  10236  fin23lem19  10335  gchi  10623  inar1  10774  inatsk  10777  avgle  12460  nnm1nn0  12519  zle0orge1  12581  uzsplit  13579  fzospliti  13670  fzouzsplit  13673  znsqcld  14133  fz1f1o  15662  fnpr2ob  17510  odcl  19447  gexcl  19491  lssvs0or  20870  lspdisj  20885  lspsncv0  20906  mdetralt  22332  filconn  23609  limccnp  25642  dgrlt  26014  logreclem  26501  atans2  26670  basellem3  26821  sqff1o  26920  nosep2o  27419  tgcgrsub2  28111  legov3  28114  colline  28165  tglowdim2ln  28167  mirbtwnhl  28196  colmid  28204  symquadlem  28205  midexlem  28208  ragperp  28233  colperp  28245  midex  28253  oppperpex  28269  hlpasch  28272  colopp  28285  lmieu  28300  lmicom  28304  lmimid  28310  lmiisolem  28312  trgcopy  28320  cgracgr  28334  cgraswap  28336  cgracol  28344  hashecclwwlkn1  29595  xlt2addrd  32236  fprodex01  32296  ssmxidl  32862  lvecdim0  32977  minplyirred  33057  zarclssn  33149  esumcvgre  33385  ordtoplem  35625  ordcmp  35637  onsucuni3  36553  dvasin  36877  eqvreldisj  37789  lkrshp4  38283  2at0mat0  38701  trlator0  39347  dia2dimlem2  40241  dia2dimlem3  40242  dochkrshp  40562  dochkrshp4  40565  lcfl6  40676  lclkrlem2k  40693  hdmap14lem6  41049  hgmapval0  41068  sticksstones12a  41281  sticksstones13  41283  acongneg2  42020  unxpwdom3  42141  dflim5  42383  mnuprdlem1  43335  mnurndlem1  43344  disjinfi  44191  xrssre  44358  icccncfext  44903  wallispilem3  45083  fourierdlem93  45215  fourierdlem101  45223  nneop  47301  itsclinecirc0  47548  itsclinecirc0b  47549  itsclinecirc0in  47550  inlinecirc02plem  47561  inlinecirc02p  47562