Theorem orcomd 869

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

Syntax hints:   → wi 4   ∨ wo 845

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 846

This theorem is referenced by:  olcd  872  orcnd  876  19.33b  1880  r19.30OLD  3111  elunnel2  4148  swopo  5600  fr2nr  5655  ordtri1  6402  ordequn  6472  ssonprc  7789  ordunpr  7828  ordunisuc2  7847  2oconcl  8522  erdisj  8776  ordtypelem7  9547  ackbij1lem18  10260  fin23lem19  10359  gchi  10647  inar1  10798  inatsk  10801  avgle  12484  nnm1nn0  12543  zle0orge1  12605  uzsplit  13605  fzospliti  13696  fzouzsplit  13699  znsqcld  14158  fz1f1o  15688  fnpr2ob  17539  odcl  19495  gexcl  19539  lssvs0or  21002  lspdisj  21017  lspsncv0  21038  mdetralt  22540  filconn  23817  limccnp  25850  dgrlt  26231  logreclem  26724  atans2  26893  basellem3  27045  sqff1o  27144  nosep2o  27645  elnns2  28245  tgcgrsub2  28455  legov3  28458  colline  28509  tglowdim2ln  28511  mirbtwnhl  28540  colmid  28548  symquadlem  28549  midexlem  28552  ragperp  28577  colperp  28589  midex  28597  oppperpex  28613  hlpasch  28616  colopp  28629  lmieu  28644  lmicom  28648  lmimid  28654  lmiisolem  28656  trgcopy  28664  cgracgr  28678  cgraswap  28680  cgracol  28688  hashecclwwlkn1  29943  xlt2addrd  32585  fprodex01  32645  ssmxidl  33249  lvecdim0  33374  minplyirred  33451  irredminply  33454  zarclssn  33544  esumcvgre  33780  ordtoplem  35989  ordcmp  36001  onsucuni3  36916  dvasin  37247  eqvreldisj  38155  lkrshp4  38649  2at0mat0  39067  trlator0  39713  dia2dimlem2  40607  dia2dimlem3  40608  dochkrshp  40928  dochkrshp4  40931  lcfl6  41042  lclkrlem2k  41059  hdmap14lem6  41415  hgmapval0  41434  sticksstones12a  41698  sticksstones13  41700  acongneg2  42463  unxpwdom3  42584  dflim5  42823  mnuprdlem1  43774  mnurndlem1  43783  disjinfi  44629  xrssre  44793  icccncfext  45338  wallispilem3  45518  fourierdlem93  45650  fourierdlem101  45658  nneop  47711  itsclinecirc0  47958  itsclinecirc0b  47959  itsclinecirc0in  47960  inlinecirc02plem  47971  inlinecirc02p  47972