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  7734  ordunpr  7770  ordunisuc2  7788  2oconcl  8432  erdisj  8695  ordtypelem7  9433  ackbij1lem18  10150  fin23lem19  10250  gchi  10539  inar1  10690  inatsk  10693  avgle  12387  nnm1nn0  12446  zle0orge1  12509  uzsplit  13516  fzospliti  13611  fzouzsplit  13614  znsqcld  14089  fz1f1o  15637  fnpr2ob  17483  odcl  19469  gexcl  19513  lssvs0or  21069  lspdisj  21084  lspsncv0  21105  mdetralt  22556  filconn  23831  limccnp  25852  dgrlt  26232  logreclem  26732  atans2  26901  basellem3  27053  sqff1o  27152  nosep2o  27654  elnns2  28321  nnm1n0s  28354  zscut0  28387  n0seo  28400  tgcgrsub2  28650  legov3  28653  colline  28704  tglowdim2ln  28706  mirbtwnhl  28735  colmid  28743  symquadlem  28744  midexlem  28747  ragperp  28772  colperp  28784  midex  28792  oppperpex  28808  hlpasch  28811  colopp  28824  lmieu  28839  lmicom  28843  lmimid  28849  lmiisolem  28851  trgcopy  28859  cgracgr  28873  cgraswap  28875  cgracol  28883  hashecclwwlkn1  30135  xlt2addrd  32820  fprodex01  32887  ssmxidl  33536  drngmxidlr  33540  lvecdim0  33744  minplyirred  33849  irredminply  33854  zarclssn  34011  esumcvgre  34229  ordtoplem  36610  ordcmp  36622  onsucuni3  37543  dvasin  37876  eqvreldisj  38870  lkrshp4  39405  2at0mat0  39822  trlator0  40468  dia2dimlem2  41362  dia2dimlem3  41363  dochkrshp  41683  dochkrshp4  41686  lcfl6  41797  lclkrlem2k  41814  hdmap14lem6  42170  hgmapval0  42189  sticksstones12a  42448  sticksstones13  42450  acongneg2  43255  unxpwdom3  43373  dflim5  43607  mnuprdlem1  44549  mnurndlem1  44558  disjinfi  45472  xrssre  45629  icccncfext  46167  wallispilem3  46347  fourierdlem93  46479  fourierdlem101  46487  grlimprclnbgrvtx  48281  gpg5nbgrvtx13starlem3  48355  nneop  48808  itsclinecirc0  49055  itsclinecirc0b  49056  itsclinecirc0in  49057  inlinecirc02plem  49068  inlinecirc02p  49069