Theorem orcomd 871

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  olcd  874  orcnd  878  19.33b  1885  elunnel2  4130  swopo  5572  fr2nr  5631  ordtri1  6385  ordequn  6456  ssonprc  7779  ordunpr  7818  ordunisuc2  7837  2oconcl  8513  erdisj  8771  ordtypelem7  9536  ackbij1lem18  10248  fin23lem19  10348  gchi  10636  inar1  10787  inatsk  10790  avgle  12481  nnm1nn0  12540  zle0orge1  12603  uzsplit  13611  fzospliti  13706  fzouzsplit  13709  znsqcld  14178  fz1f1o  15724  fnpr2ob  17570  odcl  19515  gexcl  19559  lssvs0or  21069  lspdisj  21084  lspsncv0  21105  mdetralt  22544  filconn  23819  limccnp  25842  dgrlt  26222  logreclem  26722  atans2  26891  basellem3  27043  sqff1o  27142  nosep2o  27644  elnns2  28261  n0seo  28322  tgcgrsub2  28520  legov3  28523  colline  28574  tglowdim2ln  28576  mirbtwnhl  28605  colmid  28613  symquadlem  28614  midexlem  28617  ragperp  28642  colperp  28654  midex  28662  oppperpex  28678  hlpasch  28681  colopp  28694  lmieu  28709  lmicom  28713  lmimid  28719  lmiisolem  28721  trgcopy  28729  cgracgr  28743  cgraswap  28745  cgracol  28753  hashecclwwlkn1  30004  xlt2addrd  32682  fprodex01  32750  ssmxidl  33435  drngmxidlr  33439  lvecdim0  33592  minplyirred  33691  irredminply  33696  zarclssn  33850  esumcvgre  34068  ordtoplem  36399  ordcmp  36411  onsucuni3  37331  dvasin  37674  eqvreldisj  38578  lkrshp4  39072  2at0mat0  39490  trlator0  40136  dia2dimlem2  41030  dia2dimlem3  41031  dochkrshp  41351  dochkrshp4  41354  lcfl6  41465  lclkrlem2k  41482  hdmap14lem6  41838  hgmapval0  41857  sticksstones12a  42116  sticksstones13  42118  acongneg2  42948  unxpwdom3  43066  dflim5  43300  mnuprdlem1  44244  mnurndlem1  44253  disjinfi  45164  xrssre  45323  icccncfext  45864  wallispilem3  46044  fourierdlem93  46176  fourierdlem101  46184  gpg5nbgrvtx13starlem3  48023  nneop  48454  itsclinecirc0  48701  itsclinecirc0b  48702  itsclinecirc0in  48703  inlinecirc02plem  48714  inlinecirc02p  48715