Theorem orcomd 402

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

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  olcd  407  19.33b  1802  swopo  4969  fr2nr  5016  ordtri1  5673  ordequn  5745  ssonprc  6884  ordunpr  6918  ordunisuc2  6936  2oconcl  7470  erdisj  7681  ordtypelem7  8312  ackbij1lem18  8942  fin23lem19  9041  gchi  9325  inar1  9476  inatsk  9479  avgle  11151  nnm1nn0  11211  uzsplit  12281  fzospliti  12369  fzouzsplit  12372  fz1f1o  14288  odcl  17778  gexcl  17818  lssvs0or  18931  lspdisj  18946  lspsncv0  18967  mdetralt  20233  filcon  21497  limccnp  23461  dgrlt  23826  logreclem  24300  atans2  24458  basellem3  24609  sqff1o  24708  tgcgrsub2  25290  legov3  25293  colline  25344  tglowdim2ln  25346  mirbtwnhl  25375  colmid  25383  symquadlem  25384  midexlem  25387  ragperp  25412  colperp  25421  midex  25429  oppperpex  25445  hlpasch  25448  colopp  25461  colhp  25462  lmieu  25476  lmicom  25480  lmimid  25486  lmiisolem  25488  trgcopy  25496  cgracgr  25510  cgraswap  25512  cgracol  25519  hashecclwwlkn1  26361  znsqcld  28900  xlt2addrd  28913  esumcvgre  29480  eulerpartlemgvv  29765  nobndup  31099  ordtoplem  31604  ordcmp  31616  onsucuni3  32391  dvasin  32666  unitresr  33055  lkrshp4  33413  2at0mat0  33829  trlator0  34476  dia2dimlem2  35372  dia2dimlem3  35373  dochkrshp  35693  dochkrshp4  35696  lcfl6  35807  lclkrlem2k  35824  hdmap14lem6  36183  hgmapval0  36202  acongneg2  36562  unxpwdom3  36683  elunnel2  38221  disjinfi  38375  xrssre  38505  icccncfext  38773  wallispilem3  38960  fourierdlem93  39092  fourierdlem101  39100  hashecclwwlksn1  41261  nneop  42114