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  1886  elunnel2  4104  swopo  5538  fr2nr  5596  ordtri1  6345  ordequn  6417  ssonprc  7726  ordunpr  7762  ordunisuc2  7780  2oconcl  8424  erdisj  8685  ordtypelem7  9416  ackbij1lem18  10133  fin23lem19  10233  gchi  10521  inar1  10672  inatsk  10675  avgle  12369  nnm1nn0  12428  zle0orge1  12491  uzsplit  13502  fzospliti  13597  fzouzsplit  13600  znsqcld  14075  fz1f1o  15623  fnpr2ob  17468  odcl  19454  gexcl  19498  lssvs0or  21053  lspdisj  21068  lspsncv0  21089  mdetralt  22529  filconn  23804  limccnp  25825  dgrlt  26205  logreclem  26705  atans2  26874  basellem3  27026  sqff1o  27125  nosep2o  27627  elnns2  28275  nnm1n0s  28306  n0seo  28350  tgcgrsub2  28579  legov3  28582  colline  28633  tglowdim2ln  28635  mirbtwnhl  28664  colmid  28672  symquadlem  28673  midexlem  28676  ragperp  28701  colperp  28713  midex  28721  oppperpex  28737  hlpasch  28740  colopp  28753  lmieu  28768  lmicom  28772  lmimid  28778  lmiisolem  28780  trgcopy  28788  cgracgr  28802  cgraswap  28804  cgracol  28812  hashecclwwlkn1  30064  xlt2addrd  32749  fprodex01  32815  ssmxidl  33446  drngmxidlr  33450  lvecdim0  33626  minplyirred  33731  irredminply  33736  zarclssn  33893  esumcvgre  34111  ordtoplem  36486  ordcmp  36498  onsucuni3  37418  dvasin  37750  eqvreldisj  38716  lkrshp4  39213  2at0mat0  39630  trlator0  40276  dia2dimlem2  41170  dia2dimlem3  41171  dochkrshp  41491  dochkrshp4  41494  lcfl6  41605  lclkrlem2k  41622  hdmap14lem6  41978  hgmapval0  41997  sticksstones12a  42256  sticksstones13  42258  acongneg2  43075  unxpwdom3  43193  dflim5  43427  mnuprdlem1  44370  mnurndlem1  44379  disjinfi  45294  xrssre  45452  icccncfext  45990  wallispilem3  46170  fourierdlem93  46302  fourierdlem101  46310  grlimprclnbgrvtx  48104  gpg5nbgrvtx13starlem3  48178  nneop  48632  itsclinecirc0  48879  itsclinecirc0b  48880  itsclinecirc0in  48881  inlinecirc02plem  48892  inlinecirc02p  48893