Theorem orcomd 880

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

Syntax hints:   → wi 4   ∨ wo 856

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 857

This theorem is referenced by:  olcd  883  orcnd  887  19.33b  1895  elunnel2  4099  swopo  5555  fr2nr  5613  ordtri1  6364  ordequn  6436  ssonprc  7755  ordunpr  7791  ordunisuc2  7809  2oconcl  8456  erdisj  8720  ordtypelem7  9458  ackbij1lem18  10178  fin23lem19  10279  gchi  10568  inar1  10719  inatsk  10722  avgle  12449  nnm1nn0  12508  zle0orge1  12571  uzsplit  13587  fzospliti  13683  fzouzsplit  13686  znsqcld  14161  fz1f1o  15709  fnpr2ob  17560  odcl  19548  gexcl  19592  lssvs0or  21149  lspdisj  21164  lspsncv0  21185  mdetralt  22637  filconn  23912  limccnp  25922  dgrlt  26295  logreclem  26793  atans2  26962  basellem3  27113  sqff1o  27212  nosep2o  27712  elnns2  28400  nnm1n0s  28434  zcuts0  28467  n0seo  28480  tgcgrsub2  28730  legov3  28733  colline  28784  tglowdim2ln  28786  mirbtwnhl  28815  colmid  28823  symquadlem  28824  midexlem  28827  ragperp  28852  colperp  28864  midex  28872  oppperpex  28888  hlpasch  28891  colopp  28904  lmieu  28919  lmicom  28923  lmimid  28929  lmiisolem  28931  trgcopy  28939  cgracgr  28953  cgraswap  28955  cgracol  28963  hashecclwwlkn1  30214  xlt2addrd  32900  fprodex01  32966  ssmxidl  33606  drngmxidlr  33610  dflring3  33637  lvecdim0  33848  minplyirred  33952  irredminply  33957  zarclssn  34114  esumcvgre  34332  ordtoplem  36733  ordcmp  36745  onsucuni3  37799  dvasin  38141  eqvreldisj  39135  lkrshp4  39670  2at0mat0  40087  trlator0  40733  dia2dimlem2  41627  dia2dimlem3  41628  dochkrshp  41948  dochkrshp4  41951  lcfl6  42062  lclkrlem2k  42079  hdmap14lem6  42435  hgmapval0  42454  sticksstones12a  42712  sticksstones13  42714  acongneg2  43492  unxpwdom3  43610  dflim5  43844  mnuprdlem1  44786  mnurndlem1  44795  disjinfi  45708  xrssre  45862  icccncfext  46399  wallispilem3  46579  fourierdlem93  46711  fourierdlem101  46719  grlimprclnbgrvtx  48559  gpg5nbgrvtx13starlem3  48633  nneop  49086  itsclinecirc0  49333  itsclinecirc0b  49334  itsclinecirc0in  49335  inlinecirc02plem  49346  inlinecirc02p  49347