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  1884  r19.30OLD  3108  elunnel2  4135  swopo  5583  fr2nr  5642  ordtri1  6396  ordequn  6467  ssonprc  7789  ordunpr  7828  ordunisuc2  7847  2oconcl  8523  erdisj  8781  ordtypelem7  9546  ackbij1lem18  10258  fin23lem19  10358  gchi  10646  inar1  10797  inatsk  10800  avgle  12491  nnm1nn0  12550  zle0orge1  12613  uzsplit  13618  fzospliti  13713  fzouzsplit  13716  znsqcld  14184  fz1f1o  15728  fnpr2ob  17574  odcl  19522  gexcl  19566  lssvs0or  21080  lspdisj  21095  lspsncv0  21116  mdetralt  22562  filconn  23837  limccnp  25862  dgrlt  26242  logreclem  26741  atans2  26910  basellem3  27062  sqff1o  27161  nosep2o  27663  elnns2  28280  n0seo  28341  tgcgrsub2  28539  legov3  28542  colline  28593  tglowdim2ln  28595  mirbtwnhl  28624  colmid  28632  symquadlem  28633  midexlem  28636  ragperp  28661  colperp  28673  midex  28681  oppperpex  28697  hlpasch  28700  colopp  28713  lmieu  28728  lmicom  28732  lmimid  28738  lmiisolem  28740  trgcopy  28748  cgracgr  28762  cgraswap  28764  cgracol  28772  hashecclwwlkn1  30024  xlt2addrd  32699  fprodex01  32767  ssmxidl  33437  drngmxidlr  33441  lvecdim0  33592  minplyirred  33691  irredminply  33696  zarclssn  33831  esumcvgre  34051  ordtoplem  36395  ordcmp  36407  onsucuni3  37327  dvasin  37670  eqvreldisj  38574  lkrshp4  39068  2at0mat0  39486  trlator0  40132  dia2dimlem2  41026  dia2dimlem3  41027  dochkrshp  41347  dochkrshp4  41350  lcfl6  41461  lclkrlem2k  41478  hdmap14lem6  41834  hgmapval0  41853  sticksstones12a  42117  sticksstones13  42119  acongneg2  42952  unxpwdom3  43070  dflim5  43304  mnuprdlem1  44248  mnurndlem1  44257  disjinfi  45154  xrssre  45316  icccncfext  45859  wallispilem3  46039  fourierdlem93  46171  fourierdlem101  46179  gpg5nbgrvtx13starlem3  47987  nneop  48405  itsclinecirc0  48652  itsclinecirc0b  48653  itsclinecirc0in  48654  inlinecirc02plem  48665  inlinecirc02p  48666