Theorem orcomd 867

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

Syntax hints:   → wi 4   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  olcd  870  orcnd  875  19.33b  1889  r19.30OLD  3266  swopo  5505  fr2nr  5558  ordtri1  6284  ordequn  6351  ssonprc  7614  ordunpr  7648  ordunisuc2  7666  2oconcl  8295  erdisj  8508  ordtypelem7  9213  ackbij1lem18  9924  fin23lem19  10023  gchi  10311  inar1  10462  inatsk  10465  avgle  12145  nnm1nn0  12204  zle0orge1  12266  uzsplit  13257  fzospliti  13347  fzouzsplit  13350  znsqcld  13808  fz1f1o  15350  fnpr2ob  17186  odcl  19059  gexcl  19100  lssvs0or  20287  lspdisj  20302  lspsncv0  20323  mdetralt  21665  filconn  22942  limccnp  24960  dgrlt  25332  logreclem  25817  atans2  25986  basellem3  26137  sqff1o  26236  tgcgrsub2  26860  legov3  26863  colline  26914  tglowdim2ln  26916  mirbtwnhl  26945  colmid  26953  symquadlem  26954  midexlem  26957  ragperp  26982  colperp  26994  midex  27002  oppperpex  27018  hlpasch  27021  colopp  27034  lmieu  27049  lmicom  27053  lmimid  27059  lmiisolem  27061  trgcopy  27069  cgracgr  27083  cgraswap  27085  cgracol  27093  hashecclwwlkn1  28342  xlt2addrd  30983  fprodex01  31041  ssmxidl  31544  lvecdim0  31592  zarclssn  31725  esumcvgre  31959  nosep2o  33812  ordtoplem  34551  ordcmp  34563  onsucuni3  35465  dvasin  35788  eqvreldisj  36654  lkrshp4  37049  2at0mat0  37466  trlator0  38112  dia2dimlem2  39006  dia2dimlem3  39007  dochkrshp  39327  dochkrshp4  39330  lcfl6  39441  lclkrlem2k  39458  hdmap14lem6  39814  hgmapval0  39833  sticksstones12a  40041  sticksstones13  40043  acongneg2  40715  unxpwdom3  40836  mnuprdlem1  41779  mnurndlem1  41788  elunnel2  42471  disjinfi  42620  xrssre  42777  icccncfext  43318  wallispilem3  43498  fourierdlem93  43630  fourierdlem101  43638  nneop  45760  itsclinecirc0  46007  itsclinecirc0b  46008  itsclinecirc0in  46009  inlinecirc02plem  46020  inlinecirc02p  46021