Theorem orcomd 872

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  olcd  875  orcnd  879  19.33b  1887  elunnel2  4108  swopo  5544  fr2nr  5602  ordtri1  6351  ordequn  6423  ssonprc  7735  ordunpr  7771  ordunisuc2  7789  2oconcl  8433  erdisj  8696  ordtypelem7  9434  ackbij1lem18  10151  fin23lem19  10251  gchi  10540  inar1  10691  inatsk  10694  avgle  12388  nnm1nn0  12447  zle0orge1  12510  uzsplit  13517  fzospliti  13612  fzouzsplit  13615  znsqcld  14090  fz1f1o  15638  fnpr2ob  17484  odcl  19470  gexcl  19514  lssvs0or  21070  lspdisj  21085  lspsncv0  21106  mdetralt  22557  filconn  23832  limccnp  25853  dgrlt  26233  logreclem  26733  atans2  26902  basellem3  27054  sqff1o  27153  nosep2o  27655  elnns2  28342  nnm1n0s  28376  zcuts0  28409  n0seo  28422  tgcgrsub2  28672  legov3  28675  colline  28726  tglowdim2ln  28728  mirbtwnhl  28757  colmid  28765  symquadlem  28766  midexlem  28769  ragperp  28794  colperp  28806  midex  28814  oppperpex  28830  hlpasch  28833  colopp  28846  lmieu  28861  lmicom  28865  lmimid  28871  lmiisolem  28873  trgcopy  28881  cgracgr  28895  cgraswap  28897  cgracol  28905  hashecclwwlkn1  30157  xlt2addrd  32842  fprodex01  32909  ssmxidl  33559  drngmxidlr  33563  lvecdim0  33776  minplyirred  33881  irredminply  33886  zarclssn  34043  esumcvgre  34261  ordtoplem  36642  ordcmp  36654  onsucuni3  37585  dvasin  37918  eqvreldisj  38912  lkrshp4  39447  2at0mat0  39864  trlator0  40510  dia2dimlem2  41404  dia2dimlem3  41405  dochkrshp  41725  dochkrshp4  41728  lcfl6  41839  lclkrlem2k  41856  hdmap14lem6  42212  hgmapval0  42231  sticksstones12a  42490  sticksstones13  42492  acongneg2  43297  unxpwdom3  43415  dflim5  43649  mnuprdlem1  44591  mnurndlem1  44600  disjinfi  45514  xrssre  45670  icccncfext  46208  wallispilem3  46388  fourierdlem93  46520  fourierdlem101  46528  grlimprclnbgrvtx  48322  gpg5nbgrvtx13starlem3  48396  nneop  48849  itsclinecirc0  49096  itsclinecirc0b  49097  itsclinecirc0in  49098  inlinecirc02plem  49109  inlinecirc02p  49110