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  1885  elunnel2  4118  swopo  5557  fr2nr  5615  ordtri1  6365  ordequn  6437  ssonprc  7763  ordunpr  7801  ordunisuc2  7820  2oconcl  8467  erdisj  8728  ordtypelem7  9477  ackbij1lem18  10189  fin23lem19  10289  gchi  10577  inar1  10728  inatsk  10731  avgle  12424  nnm1nn0  12483  zle0orge1  12546  uzsplit  13557  fzospliti  13652  fzouzsplit  13655  znsqcld  14127  fz1f1o  15676  fnpr2ob  17521  odcl  19466  gexcl  19510  lssvs0or  21020  lspdisj  21035  lspsncv0  21056  mdetralt  22495  filconn  23770  limccnp  25792  dgrlt  26172  logreclem  26672  atans2  26841  basellem3  26993  sqff1o  27092  nosep2o  27594  elnns2  28233  nnm1n0s  28264  n0seo  28307  tgcgrsub2  28522  legov3  28525  colline  28576  tglowdim2ln  28578  mirbtwnhl  28607  colmid  28615  symquadlem  28616  midexlem  28619  ragperp  28644  colperp  28656  midex  28664  oppperpex  28680  hlpasch  28683  colopp  28696  lmieu  28711  lmicom  28715  lmimid  28721  lmiisolem  28723  trgcopy  28731  cgracgr  28745  cgraswap  28747  cgracol  28755  hashecclwwlkn1  30006  xlt2addrd  32682  fprodex01  32750  ssmxidl  33445  drngmxidlr  33449  lvecdim0  33602  minplyirred  33701  irredminply  33706  zarclssn  33863  esumcvgre  34081  ordtoplem  36423  ordcmp  36435  onsucuni3  37355  dvasin  37698  eqvreldisj  38605  lkrshp4  39101  2at0mat0  39519  trlator0  40165  dia2dimlem2  41059  dia2dimlem3  41060  dochkrshp  41380  dochkrshp4  41383  lcfl6  41494  lclkrlem2k  41511  hdmap14lem6  41867  hgmapval0  41886  sticksstones12a  42145  sticksstones13  42147  acongneg2  42966  unxpwdom3  43084  dflim5  43318  mnuprdlem1  44261  mnurndlem1  44270  disjinfi  45186  xrssre  45344  icccncfext  45885  wallispilem3  46065  fourierdlem93  46197  fourierdlem101  46205  gpg5nbgrvtx13starlem3  48064  nneop  48515  itsclinecirc0  48762  itsclinecirc0b  48763  itsclinecirc0in  48764  inlinecirc02plem  48775  inlinecirc02p  48776