Theorem orcomd 869

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

Syntax hints:   → wi 4   ∨ wo 845

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 210  df-or 846

This theorem is referenced by:  olcd  872  orcnd  877  19.33b  1887  r19.30  3259  swopo  5454  fr2nr  5503  ordtri1  6203  ordequn  6270  ssonprc  7507  ordunpr  7541  ordunisuc2  7559  2oconcl  8139  erdisj  8352  ordtypelem7  9014  ackbij1lem18  9690  fin23lem19  9789  gchi  10077  inar1  10228  inatsk  10231  avgle  11909  nnm1nn0  11968  zle0orge1  12030  uzsplit  13021  fzospliti  13111  fzouzsplit  13114  znsqcld  13569  fz1f1o  15108  fnpr2ob  16882  odcl  18724  gexcl  18765  lssvs0or  19943  lspdisj  19958  lspsncv0  19979  mdetralt  21301  filconn  22576  limccnp  24583  dgrlt  24955  logreclem  25440  atans2  25609  basellem3  25760  sqff1o  25859  tgcgrsub2  26481  legov3  26484  colline  26535  tglowdim2ln  26537  mirbtwnhl  26566  colmid  26574  symquadlem  26575  midexlem  26578  ragperp  26603  colperp  26615  midex  26623  oppperpex  26639  hlpasch  26642  colopp  26655  lmieu  26670  lmicom  26674  lmimid  26680  lmiisolem  26682  trgcopy  26690  cgracgr  26704  cgraswap  26706  cgracol  26714  hashecclwwlkn1  27954  xlt2addrd  30598  fprodex01  30656  ssmxidl  31156  lvecdim0  31204  zarclssn  31337  esumcvgre  31571  nosep2o  33443  ordtoplem  34166  ordcmp  34178  onsucuni3  35057  dvasin  35414  eqvreldisj  36282  lkrshp4  36677  2at0mat0  37094  trlator0  37740  dia2dimlem2  38634  dia2dimlem3  38635  dochkrshp  38955  dochkrshp4  38958  lcfl6  39069  lclkrlem2k  39086  hdmap14lem6  39442  hgmapval0  39461  acongneg2  40284  unxpwdom3  40405  mnuprdlem1  41346  mnurndlem1  41355  elunnel2  42034  disjinfi  42183  xrssre  42341  icccncfext  42888  wallispilem3  43068  fourierdlem93  43200  fourierdlem101  43208  nneop  45298  itsclinecirc0  45545  itsclinecirc0b  45546  itsclinecirc0in  45547  inlinecirc02plem  45558  inlinecirc02p  45559