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 208	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 197  df-or 384

This theorem is referenced by:  olcd  407  19.33b  1853  swopo  5074  fr2nr  5121  ordtri1  5794  ordequn  5866  ssonprc  7034  ordunpr  7068  ordunisuc2  7086  2oconcl  7628  erdisj  7837  ordtypelem7  8470  ackbij1lem18  9097  fin23lem19  9196  gchi  9484  inar1  9635  inatsk  9638  avgle  11312  nnm1nn0  11372  uzsplit  12450  fzospliti  12539  fzouzsplit  12542  fz1f1o  14485  odcl  18001  gexcl  18041  lssvs0or  19158  lspdisj  19173  lspsncv0  19194  mdetralt  20462  filconn  21734  limccnp  23700  dgrlt  24067  logreclem  24545  atans2  24703  basellem3  24854  sqff1o  24953  tgcgrsub2  25535  legov3  25538  colline  25589  tglowdim2ln  25591  mirbtwnhl  25620  colmid  25628  symquadlem  25629  midexlem  25632  ragperp  25657  colperp  25666  midex  25674  oppperpex  25690  hlpasch  25693  colopp  25706  colhp  25707  lmieu  25721  lmicom  25725  lmimid  25731  lmiisolem  25733  trgcopy  25741  cgracgr  25755  cgraswap  25757  cgracol  25764  hashecclwwlkn1  27041  znsqcld  29640  xlt2addrd  29651  fprodex01  29699  esumcvgre  30281  eulerpartlemgvv  30566  ordtoplem  32559  ordcmp  32571  onsucuni3  33345  dvasin  33626  unitresr  34015  lkrshp4  34713  2at0mat0  35129  trlator0  35776  dia2dimlem2  36671  dia2dimlem3  36672  dochkrshp  36992  dochkrshp4  36995  lcfl6  37106  lclkrlem2k  37123  hdmap14lem6  37482  hgmapval0  37501  acongneg2  37861  unxpwdom3  37982  elunnel2  39512  disjinfi  39694  xrssre  39877  icccncfext  40418  wallispilem3  40602  fourierdlem93  40734  fourierdlem101  40742  nneop  42645