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 218	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 207  df-or 847

This theorem is referenced by:  olcd  873  orcnd  877  19.33b  1884  r19.30OLD  3127  elunnel2  4178  swopo  5619  fr2nr  5677  ordtri1  6428  ordequn  6498  ssonprc  7823  ordunpr  7862  ordunisuc2  7881  2oconcl  8559  erdisj  8817  ordtypelem7  9593  ackbij1lem18  10305  fin23lem19  10405  gchi  10693  inar1  10844  inatsk  10847  avgle  12535  nnm1nn0  12594  zle0orge1  12656  uzsplit  13656  fzospliti  13748  fzouzsplit  13751  znsqcld  14212  fz1f1o  15758  fnpr2ob  17618  odcl  19578  gexcl  19622  lssvs0or  21135  lspdisj  21150  lspsncv0  21171  mdetralt  22635  filconn  23912  limccnp  25946  dgrlt  26326  logreclem  26823  atans2  26992  basellem3  27144  sqff1o  27243  nosep2o  27745  elnns2  28362  n0seo  28423  tgcgrsub2  28621  legov3  28624  colline  28675  tglowdim2ln  28677  mirbtwnhl  28706  colmid  28714  symquadlem  28715  midexlem  28718  ragperp  28743  colperp  28755  midex  28763  oppperpex  28779  hlpasch  28782  colopp  28795  lmieu  28810  lmicom  28814  lmimid  28820  lmiisolem  28822  trgcopy  28830  cgracgr  28844  cgraswap  28846  cgracol  28854  hashecclwwlkn1  30109  xlt2addrd  32765  fprodex01  32829  ssmxidl  33467  drngmxidlr  33471  lvecdim0  33619  minplyirred  33704  irredminply  33707  zarclssn  33819  esumcvgre  34055  ordtoplem  36401  ordcmp  36413  onsucuni3  37333  dvasin  37664  eqvreldisj  38570  lkrshp4  39064  2at0mat0  39482  trlator0  40128  dia2dimlem2  41022  dia2dimlem3  41023  dochkrshp  41343  dochkrshp4  41346  lcfl6  41457  lclkrlem2k  41474  hdmap14lem6  41830  hgmapval0  41849  sticksstones12a  42114  sticksstones13  42116  acongneg2  42934  unxpwdom3  43052  dflim5  43291  mnuprdlem1  44241  mnurndlem1  44250  disjinfi  45099  xrssre  45263  icccncfext  45808  wallispilem3  45988  fourierdlem93  46120  fourierdlem101  46128  nneop  48260  itsclinecirc0  48507  itsclinecirc0b  48508  itsclinecirc0in  48509  inlinecirc02plem  48520  inlinecirc02p  48521