Theorem orcomd 870

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

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  olcd  873  orcnd  878  19.33b  1889  r19.30OLD  3122  elunnel2  4151  swopo  5600  fr2nr  5655  ordtri1  6398  ordequn  6468  ssonprc  7775  ordunpr  7814  ordunisuc2  7833  2oconcl  8503  erdisj  8755  ordtypelem7  9519  ackbij1lem18  10232  fin23lem19  10331  gchi  10619  inar1  10770  inatsk  10773  avgle  12454  nnm1nn0  12513  zle0orge1  12575  uzsplit  13573  fzospliti  13664  fzouzsplit  13667  znsqcld  14127  fz1f1o  15656  fnpr2ob  17504  odcl  19404  gexcl  19448  lssvs0or  20723  lspdisj  20738  lspsncv0  20759  mdetralt  22110  filconn  23387  limccnp  25408  dgrlt  25780  logreclem  26267  atans2  26436  basellem3  26587  sqff1o  26686  nosep2o  27185  tgcgrsub2  27877  legov3  27880  colline  27931  tglowdim2ln  27933  mirbtwnhl  27962  colmid  27970  symquadlem  27971  midexlem  27974  ragperp  27999  colperp  28011  midex  28019  oppperpex  28035  hlpasch  28038  colopp  28051  lmieu  28066  lmicom  28070  lmimid  28076  lmiisolem  28078  trgcopy  28086  cgracgr  28100  cgraswap  28102  cgracol  28110  hashecclwwlkn1  29361  xlt2addrd  32002  fprodex01  32062  ssmxidl  32621  lvecdim0  32722  minplyirred  32801  zarclssn  32884  esumcvgre  33120  ordtoplem  35368  ordcmp  35380  onsucuni3  36296  dvasin  36620  eqvreldisj  37532  lkrshp4  38026  2at0mat0  38444  trlator0  39090  dia2dimlem2  39984  dia2dimlem3  39985  dochkrshp  40305  dochkrshp4  40308  lcfl6  40419  lclkrlem2k  40436  hdmap14lem6  40792  hgmapval0  40811  sticksstones12a  41021  sticksstones13  41023  acongneg2  41764  unxpwdom3  41885  dflim5  42127  mnuprdlem1  43079  mnurndlem1  43088  disjinfi  43939  xrssre  44106  icccncfext  44651  wallispilem3  44831  fourierdlem93  44963  fourierdlem101  44971  nneop  47260  itsclinecirc0  47507  itsclinecirc0b  47508  itsclinecirc0in  47509  inlinecirc02plem  47520  inlinecirc02p  47521