Theorem orcomd 884

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  olcd  887  orcnd  891  19.33b  1913  elunnel2  4108  swopo  5580  fr2nr  5638  ordtri1  6394  ordequn  6466  ssonprc  7785  ordunpr  7821  ordunisuc2  7839  2oconcl  8487  erdisj  8751  ordtypelem7  9485  ackbij1lem18  10218  fin23lem19  10319  gchi  10608  inar1  10759  inatsk  10762  avgle  12485  nnm1nn0  12544  zle0orge1  12607  uzsplit  13623  fzospliti  13719  fzouzsplit  13722  znsqcld  14197  fz1f1o  15760  fnpr2ob  17611  odcl  19605  gexcl  19649  lssvs0or  21213  lspdisj  21228  lspsncv0  21249  mdetralt  22744  filconn  24019  limccnp  26029  dgrlt  26402  logreclem  26903  atans2  27072  basellem3  27223  sqff1o  27322  nosep2o  27822  elnns2  28510  nnm1n0s  28544  zcuts0  28577  n0seo  28590  tgcgrsub2  28840  legov3  28843  colline  28899  tglowdim2ln  28901  mirbtwnhl  28933  colmid  28941  symquadlem  28942  midexlem  28945  ragperp  28972  colperp  28985  midex  28993  oppperpex  29009  hlpasch  29013  colopp  29026  plngcplem  29041  plngmiropp  29050  lmieu  29067  lmicom  29071  lmimid  29077  lmiisolem  29079  trgcopy  29088  cgracgr  29102  cgraswap  29104  cgracol  29112  hashecclwwlkn1  30394  xlt2addrd  33070  fprodex01  33135  ssmxidl  33723  drngmxidlr  33726  dflring3  33753  lvecdim0  33963  minplyirred  34067  irredminply  34072  zarclssn  34229  esumcvgre  34447  ordtoplem  36890  ordcmp  36902  onsucuni3  37957  dvasin  38299  eqvreldisj  39293  lkrshp4  39828  2at0mat0  40245  trlator0  40891  dia2dimlem2  41785  dia2dimlem3  41786  dochkrshp  42106  dochkrshp4  42109  lcfl6  42220  lclkrlem2k  42237  hdmap14lem6  42593  hgmapval0  42612  sticksstones12a  42870  sticksstones13  42872  acongneg2  43652  unxpwdom3  43770  dflim5  44004  mnuprdlem1  44930  mnurndlem1  44939  disjinfi  45858  xrssre  46012  icccncfext  46549  wallispilem3  46729  fourierdlem93  46861  fourierdlem101  46869  grlimprclnbgrvtx  48709  gpg5nbgrvtx13starlem3  48783  nneop  49251  itsclinecirc0  49498  itsclinecirc0b  49499  itsclinecirc0in  49500  inlinecirc02plem  49511  inlinecirc02p  49512