Theorem orcomd 872

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  olcd  875  orcnd  879  19.33b  1887  elunnel2  4087  swopo  5539  fr2nr  5597  ordtri1  6345  ordequn  6417  ssonprc  7730  ordunpr  7766  ordunisuc2  7784  2oconcl  8427  erdisj  8690  ordtypelem7  9428  ackbij1lem18  10147  fin23lem19  10247  gchi  10536  inar1  10687  inatsk  10690  avgle  12408  nnm1nn0  12467  zle0orge1  12530  uzsplit  13539  fzospliti  13635  fzouzsplit  13638  znsqcld  14113  fz1f1o  15661  fnpr2ob  17511  odcl  19500  gexcl  19544  lssvs0or  21097  lspdisj  21112  lspsncv0  21133  mdetralt  22561  filconn  23836  limccnp  25846  dgrlt  26219  logreclem  26714  atans2  26883  basellem3  27034  sqff1o  27133  nosep2o  27634  elnns2  28321  nnm1n0s  28355  zcuts0  28388  n0seo  28401  tgcgrsub2  28651  legov3  28654  colline  28705  tglowdim2ln  28707  mirbtwnhl  28736  colmid  28744  symquadlem  28745  midexlem  28748  ragperp  28773  colperp  28785  midex  28793  oppperpex  28809  hlpasch  28812  colopp  28825  lmieu  28840  lmicom  28844  lmimid  28850  lmiisolem  28852  trgcopy  28860  cgracgr  28874  cgraswap  28876  cgracol  28884  hashecclwwlkn1  30135  xlt2addrd  32820  fprodex01  32886  ssmxidl  33522  drngmxidlr  33526  lvecdim0  33739  minplyirred  33843  irredminply  33848  zarclssn  34005  esumcvgre  34223  ordtoplem  36605  ordcmp  36617  onsucuni3  37671  dvasin  38013  eqvreldisj  39007  lkrshp4  39542  2at0mat0  39959  trlator0  40605  dia2dimlem2  41499  dia2dimlem3  41500  dochkrshp  41820  dochkrshp4  41823  lcfl6  41934  lclkrlem2k  41951  hdmap14lem6  42307  hgmapval0  42326  sticksstones12a  42584  sticksstones13  42586  acongneg2  43393  unxpwdom3  43511  dflim5  43745  mnuprdlem1  44687  mnurndlem1  44696  disjinfi  45610  xrssre  45766  icccncfext  46303  wallispilem3  46483  fourierdlem93  46615  fourierdlem101  46623  grlimprclnbgrvtx  48463  gpg5nbgrvtx13starlem3  48537  nneop  48990  itsclinecirc0  49237  itsclinecirc0b  49238  itsclinecirc0in  49239  inlinecirc02plem  49250  inlinecirc02p  49251