Theorem orcomd 868

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

Syntax hints:   → wi 4   ∨ wo 844

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 845

This theorem is referenced by:  olcd  871  orcnd  876  19.33b  1889  r19.30OLD  3270  swopo  5515  fr2nr  5568  ordtri1  6303  ordequn  6370  ssonprc  7646  ordunpr  7682  ordunisuc2  7700  2oconcl  8342  erdisj  8559  ordtypelem7  9292  ackbij1lem18  10002  fin23lem19  10101  gchi  10389  inar1  10540  inatsk  10543  avgle  12224  nnm1nn0  12283  zle0orge1  12345  uzsplit  13337  fzospliti  13428  fzouzsplit  13431  znsqcld  13889  fz1f1o  15431  fnpr2ob  17278  odcl  19153  gexcl  19194  lssvs0or  20381  lspdisj  20396  lspsncv0  20417  mdetralt  21766  filconn  23043  limccnp  25064  dgrlt  25436  logreclem  25921  atans2  26090  basellem3  26241  sqff1o  26340  tgcgrsub2  26965  legov3  26968  colline  27019  tglowdim2ln  27021  mirbtwnhl  27050  colmid  27058  symquadlem  27059  midexlem  27062  ragperp  27087  colperp  27099  midex  27107  oppperpex  27123  hlpasch  27126  colopp  27139  lmieu  27154  lmicom  27158  lmimid  27164  lmiisolem  27166  trgcopy  27174  cgracgr  27188  cgraswap  27190  cgracol  27198  hashecclwwlkn1  28450  xlt2addrd  31090  fprodex01  31148  ssmxidl  31651  lvecdim0  31699  zarclssn  31832  esumcvgre  32068  nosep2o  33894  ordtoplem  34633  ordcmp  34645  onsucuni3  35547  dvasin  35870  eqvreldisj  36734  lkrshp4  37129  2at0mat0  37546  trlator0  38192  dia2dimlem2  39086  dia2dimlem3  39087  dochkrshp  39407  dochkrshp4  39410  lcfl6  39521  lclkrlem2k  39538  hdmap14lem6  39894  hgmapval0  39913  sticksstones12a  40120  sticksstones13  40122  acongneg2  40806  unxpwdom3  40927  mnuprdlem1  41897  mnurndlem1  41906  elunnel2  42589  disjinfi  42738  xrssre  42894  icccncfext  43435  wallispilem3  43615  fourierdlem93  43747  fourierdlem101  43755  nneop  45883  itsclinecirc0  46130  itsclinecirc0b  46131  itsclinecirc0in  46132  inlinecirc02plem  46143  inlinecirc02p  46144