Theorem orcomd 869

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

Syntax hints:   → wi 4   ∨ wo 845

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 846

This theorem is referenced by:  olcd  872  orcnd  876  19.33b  1880  r19.30OLD  3110  elunnel2  4147  swopo  5601  fr2nr  5656  ordtri1  6404  ordequn  6474  ssonprc  7791  ordunpr  7830  ordunisuc2  7849  2oconcl  8524  erdisj  8778  ordtypelem7  9554  ackbij1lem18  10267  fin23lem19  10366  gchi  10654  inar1  10805  inatsk  10808  avgle  12492  nnm1nn0  12551  zle0orge1  12613  uzsplit  13613  fzospliti  13704  fzouzsplit  13707  znsqcld  14167  fz1f1o  15697  fnpr2ob  17548  odcl  19508  gexcl  19552  lssvs0or  21015  lspdisj  21030  lspsncv0  21051  mdetralt  22559  filconn  23836  limccnp  25869  dgrlt  26251  logreclem  26744  atans2  26913  basellem3  27065  sqff1o  27164  nosep2o  27666  elnns2  28266  tgcgrsub2  28476  legov3  28479  colline  28530  tglowdim2ln  28532  mirbtwnhl  28561  colmid  28569  symquadlem  28570  midexlem  28573  ragperp  28598  colperp  28610  midex  28618  oppperpex  28634  hlpasch  28637  colopp  28650  lmieu  28665  lmicom  28669  lmimid  28675  lmiisolem  28677  trgcopy  28685  cgracgr  28699  cgraswap  28701  cgracol  28709  hashecclwwlkn1  29964  xlt2addrd  32615  fprodex01  32678  ssmxidl  33291  drngmxidlr  33295  lvecdim0  33437  minplyirred  33514  irredminply  33517  zarclssn  33607  esumcvgre  33843  ordtoplem  36052  ordcmp  36064  onsucuni3  36979  dvasin  37310  eqvreldisj  38218  lkrshp4  38712  2at0mat0  39130  trlator0  39776  dia2dimlem2  40670  dia2dimlem3  40671  dochkrshp  40991  dochkrshp4  40994  lcfl6  41105  lclkrlem2k  41122  hdmap14lem6  41478  hgmapval0  41497  sticksstones12a  41762  sticksstones13  41764  acongneg2  42542  unxpwdom3  42663  dflim5  42902  mnuprdlem1  43853  mnurndlem1  43862  disjinfi  44706  xrssre  44870  icccncfext  45415  wallispilem3  45595  fourierdlem93  45727  fourierdlem101  45735  nneop  47787  itsclinecirc0  48034  itsclinecirc0b  48035  itsclinecirc0in  48036  inlinecirc02plem  48047  inlinecirc02p  48048