Theorem orcomd 867

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  olcd  870  orcnd  875  19.33b  1886  r19.30  3338  swopo  5484  fr2nr  5533  ordtri1  6224  ordequn  6291  ssonprc  7507  ordunpr  7541  ordunisuc2  7559  2oconcl  8128  erdisj  8341  ordtypelem7  8988  ackbij1lem18  9659  fin23lem19  9758  gchi  10046  inar1  10197  inatsk  10200  avgle  11880  nnm1nn0  11939  zle0orge1  11999  uzsplit  12980  fzospliti  13070  fzouzsplit  13073  znsqcld  13527  fz1f1o  15067  fnpr2ob  16831  odcl  18664  gexcl  18705  lssvs0or  19882  lspdisj  19897  lspsncv0  19918  mdetralt  21217  filconn  22491  limccnp  24489  dgrlt  24856  logreclem  25340  atans2  25509  basellem3  25660  sqff1o  25759  tgcgrsub2  26381  legov3  26384  colline  26435  tglowdim2ln  26437  mirbtwnhl  26466  colmid  26474  symquadlem  26475  midexlem  26478  ragperp  26503  colperp  26515  midex  26523  oppperpex  26539  hlpasch  26542  colopp  26555  lmieu  26570  lmicom  26574  lmimid  26580  lmiisolem  26582  trgcopy  26590  cgracgr  26604  cgraswap  26606  cgracol  26614  hashecclwwlkn1  27856  xlt2addrd  30482  fprodex01  30541  ssmxidl  30979  lvecdim0  31005  esumcvgre  31350  ordtoplem  33783  ordcmp  33795  onsucuni3  34651  dvasin  34993  eqvreldisj  35864  lkrshp4  36259  2at0mat0  36676  trlator0  37322  dia2dimlem2  38216  dia2dimlem3  38217  dochkrshp  38537  dochkrshp4  38540  lcfl6  38651  lclkrlem2k  38668  hdmap14lem6  39024  hgmapval0  39043  acongneg2  39594  unxpwdom3  39715  mnuprdlem1  40628  mnurndlem1  40637  elunnel2  41316  disjinfi  41474  xrssre  41636  icccncfext  42190  wallispilem3  42372  fourierdlem93  42504  fourierdlem101  42512  nneop  44606  itsclinecirc0  44780  itsclinecirc0b  44781  itsclinecirc0in  44782  inlinecirc02plem  44793  inlinecirc02p  44794