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  1886  elunnel2  4103  swopo  5533  fr2nr  5591  ordtri1  6335  ordequn  6407  ssonprc  7715  ordunpr  7751  ordunisuc2  7769  2oconcl  8413  erdisj  8674  ordtypelem7  9405  ackbij1lem18  10119  fin23lem19  10219  gchi  10507  inar1  10658  inatsk  10661  avgle  12355  nnm1nn0  12414  zle0orge1  12477  uzsplit  13488  fzospliti  13583  fzouzsplit  13586  znsqcld  14061  fz1f1o  15609  fnpr2ob  17454  odcl  19441  gexcl  19485  lssvs0or  21040  lspdisj  21055  lspsncv0  21076  mdetralt  22516  filconn  23791  limccnp  25812  dgrlt  26192  logreclem  26692  atans2  26861  basellem3  27013  sqff1o  27112  nosep2o  27614  elnns2  28262  nnm1n0s  28293  n0seo  28337  tgcgrsub2  28566  legov3  28569  colline  28620  tglowdim2ln  28622  mirbtwnhl  28651  colmid  28659  symquadlem  28660  midexlem  28663  ragperp  28688  colperp  28700  midex  28708  oppperpex  28724  hlpasch  28727  colopp  28740  lmieu  28755  lmicom  28759  lmimid  28765  lmiisolem  28767  trgcopy  28775  cgracgr  28789  cgraswap  28791  cgracol  28799  hashecclwwlkn1  30047  xlt2addrd  32732  fprodex01  32798  ssmxidl  33429  drngmxidlr  33433  lvecdim0  33609  minplyirred  33714  irredminply  33719  zarclssn  33876  esumcvgre  34094  ordtoplem  36448  ordcmp  36460  onsucuni3  37380  dvasin  37723  eqvreldisj  38630  lkrshp4  39126  2at0mat0  39543  trlator0  40189  dia2dimlem2  41083  dia2dimlem3  41084  dochkrshp  41404  dochkrshp4  41407  lcfl6  41518  lclkrlem2k  41535  hdmap14lem6  41891  hgmapval0  41910  sticksstones12a  42169  sticksstones13  42171  acongneg2  42989  unxpwdom3  43107  dflim5  43341  mnuprdlem1  44284  mnurndlem1  44293  disjinfi  45208  xrssre  45366  icccncfext  45904  wallispilem3  46084  fourierdlem93  46216  fourierdlem101  46224  grlimprclnbgrvtx  48009  gpg5nbgrvtx13starlem3  48083  nneop  48537  itsclinecirc0  48784  itsclinecirc0b  48785  itsclinecirc0in  48786  inlinecirc02plem  48797  inlinecirc02p  48798