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 221	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 210  df-or 845

This theorem is referenced by:  olcd  871  orcnd  876  19.33b  1886  r19.30  3293  swopo  5448  fr2nr  5497  ordtri1  6192  ordequn  6259  ssonprc  7487  ordunpr  7521  ordunisuc2  7539  2oconcl  8111  erdisj  8324  ordtypelem7  8972  ackbij1lem18  9648  fin23lem19  9747  gchi  10035  inar1  10186  inatsk  10189  avgle  11867  nnm1nn0  11926  zle0orge1  11986  uzsplit  12974  fzospliti  13064  fzouzsplit  13067  znsqcld  13522  fz1f1o  15059  fnpr2ob  16823  odcl  18656  gexcl  18697  lssvs0or  19875  lspdisj  19890  lspsncv0  19911  mdetralt  21213  filconn  22488  limccnp  24494  dgrlt  24863  logreclem  25348  atans2  25517  basellem3  25668  sqff1o  25767  tgcgrsub2  26389  legov3  26392  colline  26443  tglowdim2ln  26445  mirbtwnhl  26474  colmid  26482  symquadlem  26483  midexlem  26486  ragperp  26511  colperp  26523  midex  26531  oppperpex  26547  hlpasch  26550  colopp  26563  lmieu  26578  lmicom  26582  lmimid  26588  lmiisolem  26590  trgcopy  26598  cgracgr  26612  cgraswap  26614  cgracol  26622  hashecclwwlkn1  27862  xlt2addrd  30508  fprodex01  30567  ssmxidl  31050  lvecdim0  31093  zarclssn  31226  esumcvgre  31460  ordtoplem  33896  ordcmp  33908  onsucuni3  34784  dvasin  35141  eqvreldisj  36009  lkrshp4  36404  2at0mat0  36821  trlator0  37467  dia2dimlem2  38361  dia2dimlem3  38362  dochkrshp  38682  dochkrshp4  38685  lcfl6  38796  lclkrlem2k  38813  hdmap14lem6  39169  hgmapval0  39188  acongneg2  39918  unxpwdom3  40039  mnuprdlem1  40980  mnurndlem1  40989  elunnel2  41668  disjinfi  41820  xrssre  41980  icccncfext  42529  wallispilem3  42709  fourierdlem93  42841  fourierdlem101  42849  nneop  44940  itsclinecirc0  45187  itsclinecirc0b  45188  itsclinecirc0in  45189  inlinecirc02plem  45200  inlinecirc02p  45201