Theorem orcomd 885

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  olcd  888  orcnd  892  19.33b  1918  elunnel2  4105  swopo  5578  fr2nr  5636  ordtri1  6395  ordequn  6467  ssonprc  7789  ordunpr  7825  ordunisuc2  7843  2oconcl  8493  erdisj  8757  ordtypelem7  9499  ackbij1lem18  10241  fin23lem19  10341  gchi  10636  inar1  10787  inatsk  10790  avgle  12513  nnm1nn0  12572  zle0orge1  12635  uzsplit  13653  fzospliti  13749  fzouzsplit  13752  znsqcld  14228  fz1f1o  15798  fnpr2ob  17648  odcl  19664  gexcl  19708  lssvs0or  21298  lspdisj  21313  lspsncv0  21334  mdetralt  22831  filconn  24110  limccnp  26120  dgrlt  26493  logreclem  26997  atans2  27166  basellem3  27317  sqff1o  27416  nosep2o  27916  elnns2  28604  nnm1n0s  28638  zcuts0  28671  n0seo  28684  tgcgrsub2  28935  legov3  28938  tghlsub  28963  colline  28995  tglowdim2ln  28997  mirbtwnhl  29029  colmid  29037  symquadlem  29038  midexlem  29041  ragperp  29069  colperp  29082  midex  29090  oppperpex  29106  hlpasch  29111  colopp  29124  plngcplem  29140  plngmiropp  29149  lmieu  29166  lmicom  29170  lmimid  29176  lmiisolem  29178  trgcopy  29188  cgracgr  29202  cgraswap  29204  cgracol  29213  hashecclwwlkn1  30533  xlt2addrd  33217  fprodex01  33282  ssmxidl  33864  drngmxidlr  33867  dflring3  33894  lvecdim0  34104  minplyirred  34208  irredminply  34213  zarclssn  34370  esumcvgre  34588  ordtoplem  37041  ordcmp  37053  onsucuni3  38108  dvasin  38440  eqvreldisj  39433  lkrshp4  39968  2at0mat0  40385  trlator0  41031  dia2dimlem2  41925  dia2dimlem3  41926  dochkrshp  42246  dochkrshp4  42249  lcfl6  42360  lclkrlem2k  42377  hdmap14lem6  42733  hgmapval0  42752  sticksstones12a  43010  sticksstones13  43012  acongneg2  43805  unxpwdom3  43923  dflim5  44157  mnuprdlem1  45083  mnurndlem1  45092  disjinfi  46011  xrssre  46165  icccncfext  46702  wallispilem3  46882  fourierdlem93  47014  fourierdlem101  47022  grlimprclnbgrvtx  48902  gpg5nbgrvtx13starlem3  48976  nneop  49443  itsclinecirc0  49690  itsclinecirc0b  49691  itsclinecirc0in  49692  inlinecirc02plem  49703  inlinecirc02p  49704