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  1885  r19.30OLD  3121  elunnel2  4155  swopo  5603  fr2nr  5662  ordtri1  6417  ordequn  6487  ssonprc  7807  ordunpr  7846  ordunisuc2  7865  2oconcl  8541  erdisj  8799  ordtypelem7  9564  ackbij1lem18  10276  fin23lem19  10376  gchi  10664  inar1  10815  inatsk  10818  avgle  12508  nnm1nn0  12567  zle0orge1  12630  uzsplit  13636  fzospliti  13731  fzouzsplit  13734  znsqcld  14202  fz1f1o  15746  fnpr2ob  17603  odcl  19554  gexcl  19598  lssvs0or  21112  lspdisj  21127  lspsncv0  21148  mdetralt  22614  filconn  23891  limccnp  25926  dgrlt  26306  logreclem  26805  atans2  26974  basellem3  27126  sqff1o  27225  nosep2o  27727  elnns2  28344  n0seo  28405  tgcgrsub2  28603  legov3  28606  colline  28657  tglowdim2ln  28659  mirbtwnhl  28688  colmid  28696  symquadlem  28697  midexlem  28700  ragperp  28725  colperp  28737  midex  28745  oppperpex  28761  hlpasch  28764  colopp  28777  lmieu  28792  lmicom  28796  lmimid  28802  lmiisolem  28804  trgcopy  28812  cgracgr  28826  cgraswap  28828  cgracol  28836  hashecclwwlkn1  30096  xlt2addrd  32762  fprodex01  32827  ssmxidl  33502  drngmxidlr  33506  lvecdim0  33657  minplyirred  33754  irredminply  33757  zarclssn  33872  esumcvgre  34092  ordtoplem  36436  ordcmp  36448  onsucuni3  37368  dvasin  37711  eqvreldisj  38615  lkrshp4  39109  2at0mat0  39527  trlator0  40173  dia2dimlem2  41067  dia2dimlem3  41068  dochkrshp  41388  dochkrshp4  41391  lcfl6  41502  lclkrlem2k  41519  hdmap14lem6  41875  hgmapval0  41894  sticksstones12a  42158  sticksstones13  42160  acongneg2  42989  unxpwdom3  43107  dflim5  43342  mnuprdlem1  44291  mnurndlem1  44300  disjinfi  45197  xrssre  45359  icccncfext  45902  wallispilem3  46082  fourierdlem93  46214  fourierdlem101  46222  gpg5nbgrvtx13starlem3  48029  nneop  48447  itsclinecirc0  48694  itsclinecirc0b  48695  itsclinecirc0in  48696  inlinecirc02plem  48707  inlinecirc02p  48708