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  4096  swopo  5550  fr2nr  5608  ordtri1  6357  ordequn  6429  ssonprc  7741  ordunpr  7777  ordunisuc2  7795  2oconcl  8438  erdisj  8701  ordtypelem7  9439  ackbij1lem18  10158  fin23lem19  10258  gchi  10547  inar1  10698  inatsk  10701  avgle  12419  nnm1nn0  12478  zle0orge1  12541  uzsplit  13550  fzospliti  13646  fzouzsplit  13649  znsqcld  14124  fz1f1o  15672  fnpr2ob  17522  odcl  19511  gexcl  19555  lssvs0or  21108  lspdisj  21123  lspsncv0  21144  mdetralt  22573  filconn  23848  limccnp  25858  dgrlt  26231  logreclem  26726  atans2  26895  basellem3  27046  sqff1o  27145  nosep2o  27646  elnns2  28333  nnm1n0s  28367  zcuts0  28400  n0seo  28413  tgcgrsub2  28663  legov3  28666  colline  28717  tglowdim2ln  28719  mirbtwnhl  28748  colmid  28756  symquadlem  28757  midexlem  28760  ragperp  28785  colperp  28797  midex  28805  oppperpex  28821  hlpasch  28824  colopp  28837  lmieu  28852  lmicom  28856  lmimid  28862  lmiisolem  28864  trgcopy  28872  cgracgr  28886  cgraswap  28888  cgracol  28896  hashecclwwlkn1  30147  xlt2addrd  32832  fprodex01  32898  ssmxidl  33534  drngmxidlr  33538  lvecdim0  33751  minplyirred  33855  irredminply  33860  zarclssn  34017  esumcvgre  34235  ordtoplem  36617  ordcmp  36629  onsucuni3  37683  dvasin  38025  eqvreldisj  39019  lkrshp4  39554  2at0mat0  39971  trlator0  40617  dia2dimlem2  41511  dia2dimlem3  41512  dochkrshp  41832  dochkrshp4  41835  lcfl6  41946  lclkrlem2k  41963  hdmap14lem6  42319  hgmapval0  42338  sticksstones12a  42596  sticksstones13  42598  acongneg2  43405  unxpwdom3  43523  dflim5  43757  mnuprdlem1  44699  mnurndlem1  44708  disjinfi  45622  xrssre  45778  icccncfext  46315  wallispilem3  46495  fourierdlem93  46627  fourierdlem101  46635  grlimprclnbgrvtx  48469  gpg5nbgrvtx13starlem3  48543  nneop  48996  itsclinecirc0  49243  itsclinecirc0b  49244  itsclinecirc0in  49245  inlinecirc02plem  49256  inlinecirc02p  49257