Theorem orcomd 872

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  olcd  875  orcnd  879  19.33b  1887  elunnel2  4096  swopo  5541  fr2nr  5599  ordtri1  6348  ordequn  6420  ssonprc  7732  ordunpr  7768  ordunisuc2  7786  2oconcl  8429  erdisj  8692  ordtypelem7  9430  ackbij1lem18  10147  fin23lem19  10247  gchi  10536  inar1  10687  inatsk  10690  avgle  12384  nnm1nn0  12443  zle0orge1  12506  uzsplit  13513  fzospliti  13608  fzouzsplit  13611  znsqcld  14086  fz1f1o  15634  fnpr2ob  17480  odcl  19469  gexcl  19513  lssvs0or  21067  lspdisj  21082  lspsncv0  21103  mdetralt  22551  filconn  23826  limccnp  25836  dgrlt  26212  logreclem  26712  atans2  26881  basellem3  27033  sqff1o  27132  nosep2o  27634  elnns2  28321  nnm1n0s  28355  zcuts0  28388  n0seo  28401  tgcgrsub2  28651  legov3  28654  colline  28705  tglowdim2ln  28707  mirbtwnhl  28736  colmid  28744  symquadlem  28745  midexlem  28748  ragperp  28773  colperp  28785  midex  28793  oppperpex  28809  hlpasch  28812  colopp  28825  lmieu  28840  lmicom  28844  lmimid  28850  lmiisolem  28852  trgcopy  28860  cgracgr  28874  cgraswap  28876  cgracol  28884  hashecclwwlkn1  30136  xlt2addrd  32822  fprodex01  32889  ssmxidl  33539  drngmxidlr  33543  lvecdim0  33756  minplyirred  33861  irredminply  33866  zarclssn  34023  esumcvgre  34241  ordtoplem  36623  ordcmp  36635  onsucuni3  37679  dvasin  38016  eqvreldisj  39010  lkrshp4  39545  2at0mat0  39962  trlator0  40608  dia2dimlem2  41502  dia2dimlem3  41503  dochkrshp  41823  dochkrshp4  41826  lcfl6  41937  lclkrlem2k  41954  hdmap14lem6  42310  hgmapval0  42329  sticksstones12a  42588  sticksstones13  42590  acongneg2  43408  unxpwdom3  43526  dflim5  43760  mnuprdlem1  44702  mnurndlem1  44711  disjinfi  45625  xrssre  45781  icccncfext  46319  wallispilem3  46499  fourierdlem93  46631  fourierdlem101  46639  grlimprclnbgrvtx  48433  gpg5nbgrvtx13starlem3  48507  nneop  48960  itsclinecirc0  49207  itsclinecirc0b  49208  itsclinecirc0in  49209  inlinecirc02plem  49220  inlinecirc02p  49221