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  4101  swopo  5566  fr2nr  5624  ordtri1  6385  ordequn  6457  ssonprc  7784  ordunpr  7820  ordunisuc2  7838  2oconcl  8489  erdisj  8753  ordtypelem7  9496  ackbij1lem18  10285  fin23lem19  10385  gchi  10680  inar1  10831  inatsk  10834  avgle  12557  nnm1nn0  12616  zle0orge1  12679  uzsplit  13698  fzospliti  13794  fzouzsplit  13797  znsqcld  14273  fz1f1o  15843  fnpr2ob  17691  odcl  19711  gexcl  19755  lssvs0or  21349  lspdisj  21364  lspsncv0  21385  mdetralt  22884  filconn  24163  limccnp  26172  dgrlt  26546  logreclem  27053  atans2  27222  basellem3  27373  sqff1o  27472  nosep2o  27972  elnns2  28660  nnm1n0s  28694  zcuts0  28727  n0seo  28740  tgcgrsub2  28991  legov3  28994  tghlsub  29019  colline  29051  tglowdim2ln  29053  mirbtwnhl  29085  colmid  29093  symquadlem  29094  midexlem  29097  ragperp  29125  colperp  29138  midex  29146  oppperpex  29162  hlpasch  29167  colopp  29180  plngcplem  29196  plngmiropp  29205  lmieu  29222  lmicom  29226  lmimid  29232  lmiisolem  29234  trgcopy  29244  cgracgr  29258  cgraswap  29260  cgracol  29269  hashecclwwlkn1  30601  xlt2addrd  33284  fprodex01  33349  ssmxidl  33932  drngmxidlr  33935  dflring3  33962  lvecdim0  34172  minplyirred  34276  irredminply  34281  zarclssn  34438  esumcvgre  34656  ordtoplem  37145  ordcmp  37157  onsucuni3  38210  dvasin  38542  eqvreldisj  39550  lkrshp4  40085  2at0mat0  40502  trlator0  41148  dia2dimlem2  42042  dia2dimlem3  42043  dochkrshp  42363  dochkrshp4  42366  lcfl6  42477  lclkrlem2k  42494  hdmap14lem6  42850  hgmapval0  42869  sticksstones12a  43127  sticksstones13  43129  acongneg2  43922  unxpwdom3  44040  dflim5  44274  mnuprdlem1  45200  mnurndlem1  45209  disjinfi  46128  xrssre  46282  icccncfext  46819  wallispilem3  46999  fourierdlem93  47131  fourierdlem101  47139  grlimprclnbgrvtx  49019  gpg5nbgrvtx13starlem3  49093  nneop  49560  itsclinecirc0  49807  itsclinecirc0b  49808  itsclinecirc0in  49809  inlinecirc02plem  49820  inlinecirc02p  49821