Theorem orcomd 889

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

Syntax hints:   → wi 4   ∨ wo 865

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 198  df-or 866

This theorem is referenced by:  olcd  892  19.33b  1975  swopo  5249  fr2nr  5296  ordtri1  5976  ordequn  6044  ssonprc  7225  ordunpr  7259  ordunisuc2  7277  2oconcl  7823  erdisj  8032  ordtypelem7  8671  ackbij1lem18  9347  fin23lem19  9446  gchi  9734  inar1  9885  inatsk  9888  avgle  11544  nnm1nn0  11603  uzsplit  12638  fzospliti  12727  fzouzsplit  12730  fz1f1o  14667  odcl  18159  gexcl  18199  lssvs0or  19320  lspdisj  19335  lspsncv0  19357  lspsncv0OLD  19358  mdetralt  20629  filconn  21904  limccnp  23875  dgrlt  24242  logreclem  24720  atans2  24878  basellem3  25029  sqff1o  25128  tgcgrsub2  25710  legov3  25713  colline  25764  tglowdim2ln  25766  mirbtwnhl  25795  colmid  25803  symquadlem  25804  midexlem  25807  ragperp  25832  colperp  25841  midex  25849  oppperpex  25865  hlpasch  25868  colopp  25881  colhp  25882  lmieu  25896  lmicom  25900  lmimid  25906  lmiisolem  25908  trgcopy  25916  cgracgr  25930  cgraswap  25932  cgracol  25939  hashecclwwlkn1  27234  znsqcld  29845  xlt2addrd  29856  fprodex01  29904  esumcvgre  30484  eulerpartlemgvv  30769  ordtoplem  32756  ordcmp  32768  onsucuni3  33533  dvasin  33810  unitresr  34198  lkrshp4  34890  2at0mat0  35307  trlator0  35953  dia2dimlem2  36847  dia2dimlem3  36848  dochkrshp  37168  dochkrshp4  37171  lcfl6  37282  lclkrlem2k  37299  hdmap14lem6  37655  hgmapval0  37674  acongneg2  38046  unxpwdom3  38167  elunnel2  39693  disjinfi  39870  xrssre  40045  icccncfext  40581  wallispilem3  40764  fourierdlem93  40896  fourierdlem101  40904  nneop  42889