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  4108  swopo  5542  fr2nr  5600  ordtri1  6344  ordequn  6416  ssonprc  7727  ordunpr  7765  ordunisuc2  7784  2oconcl  8428  erdisj  8689  ordtypelem7  9435  ackbij1lem18  10149  fin23lem19  10249  gchi  10537  inar1  10688  inatsk  10691  avgle  12384  nnm1nn0  12443  zle0orge1  12506  uzsplit  13517  fzospliti  13612  fzouzsplit  13615  znsqcld  14087  fz1f1o  15635  fnpr2ob  17480  odcl  19433  gexcl  19477  lssvs0or  21035  lspdisj  21050  lspsncv0  21071  mdetralt  22511  filconn  23786  limccnp  25808  dgrlt  26188  logreclem  26688  atans2  26857  basellem3  27009  sqff1o  27108  nosep2o  27610  elnns2  28256  nnm1n0s  28287  n0seo  28331  tgcgrsub2  28558  legov3  28561  colline  28612  tglowdim2ln  28614  mirbtwnhl  28643  colmid  28651  symquadlem  28652  midexlem  28655  ragperp  28680  colperp  28692  midex  28700  oppperpex  28716  hlpasch  28719  colopp  28732  lmieu  28747  lmicom  28751  lmimid  28757  lmiisolem  28759  trgcopy  28767  cgracgr  28781  cgraswap  28783  cgracol  28791  hashecclwwlkn1  30039  xlt2addrd  32715  fprodex01  32783  ssmxidl  33421  drngmxidlr  33425  lvecdim0  33578  minplyirred  33677  irredminply  33682  zarclssn  33839  esumcvgre  34057  ordtoplem  36408  ordcmp  36420  onsucuni3  37340  dvasin  37683  eqvreldisj  38590  lkrshp4  39086  2at0mat0  39504  trlator0  40150  dia2dimlem2  41044  dia2dimlem3  41045  dochkrshp  41365  dochkrshp4  41368  lcfl6  41479  lclkrlem2k  41496  hdmap14lem6  41852  hgmapval0  41871  sticksstones12a  42130  sticksstones13  42132  acongneg2  42950  unxpwdom3  43068  dflim5  43302  mnuprdlem1  44245  mnurndlem1  44254  disjinfi  45170  xrssre  45328  icccncfext  45869  wallispilem3  46049  fourierdlem93  46181  fourierdlem101  46189  gpg5nbgrvtx13starlem3  48048  nneop  48499  itsclinecirc0  48746  itsclinecirc0b  48747  itsclinecirc0in  48748  inlinecirc02plem  48759  inlinecirc02p  48760