Theorem orcomd 871

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

Syntax hints:   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  olcd  874  orcnd  878  19.33b  1882  r19.30OLD  3118  elunnel2  4164  swopo  5607  fr2nr  5665  ordtri1  6418  ordequn  6488  ssonprc  7806  ordunpr  7845  ordunisuc2  7864  2oconcl  8539  erdisj  8797  ordtypelem7  9561  ackbij1lem18  10273  fin23lem19  10373  gchi  10661  inar1  10812  inatsk  10815  avgle  12505  nnm1nn0  12564  zle0orge1  12627  uzsplit  13632  fzospliti  13727  fzouzsplit  13730  znsqcld  14198  fz1f1o  15742  fnpr2ob  17604  odcl  19568  gexcl  19612  lssvs0or  21129  lspdisj  21144  lspsncv0  21165  mdetralt  22629  filconn  23906  limccnp  25940  dgrlt  26320  logreclem  26819  atans2  26988  basellem3  27140  sqff1o  27239  nosep2o  27741  elnns2  28358  n0seo  28419  tgcgrsub2  28617  legov3  28620  colline  28671  tglowdim2ln  28673  mirbtwnhl  28702  colmid  28710  symquadlem  28711  midexlem  28714  ragperp  28739  colperp  28751  midex  28759  oppperpex  28775  hlpasch  28778  colopp  28791  lmieu  28806  lmicom  28810  lmimid  28816  lmiisolem  28818  trgcopy  28826  cgracgr  28840  cgraswap  28842  cgracol  28850  hashecclwwlkn1  30105  xlt2addrd  32768  fprodex01  32831  ssmxidl  33481  drngmxidlr  33485  lvecdim0  33633  minplyirred  33718  irredminply  33721  zarclssn  33833  esumcvgre  34071  ordtoplem  36417  ordcmp  36429  onsucuni3  37349  dvasin  37690  eqvreldisj  38595  lkrshp4  39089  2at0mat0  39507  trlator0  40153  dia2dimlem2  41047  dia2dimlem3  41048  dochkrshp  41368  dochkrshp4  41371  lcfl6  41482  lclkrlem2k  41499  hdmap14lem6  41855  hgmapval0  41874  sticksstones12a  42138  sticksstones13  42140  acongneg2  42965  unxpwdom3  43083  dflim5  43318  mnuprdlem1  44267  mnurndlem1  44276  disjinfi  45134  xrssre  45297  icccncfext  45842  wallispilem3  46022  fourierdlem93  46154  fourierdlem101  46162  gpg5nbgrvtx13starlem3  47963  nneop  48375  itsclinecirc0  48622  itsclinecirc0b  48623  itsclinecirc0in  48624  inlinecirc02plem  48635  inlinecirc02p  48636