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  877  19.33b  1881  r19.30OLD  3116  elunnel2  4146  swopo  5595  fr2nr  5650  ordtri1  6396  ordequn  6466  ssonprc  7784  ordunpr  7823  ordunisuc2  7842  2oconcl  8517  erdisj  8771  ordtypelem7  9541  ackbij1lem18  10254  fin23lem19  10353  gchi  10641  inar1  10792  inatsk  10795  avgle  12478  nnm1nn0  12537  zle0orge1  12599  uzsplit  13599  fzospliti  13690  fzouzsplit  13693  znsqcld  14152  fz1f1o  15682  fnpr2ob  17533  odcl  19484  gexcl  19528  lssvs0or  20991  lspdisj  21006  lspsncv0  21027  mdetralt  22503  filconn  23780  limccnp  25813  dgrlt  26194  logreclem  26687  atans2  26856  basellem3  27008  sqff1o  27107  nosep2o  27608  elnns2  28202  tgcgrsub2  28392  legov3  28395  colline  28446  tglowdim2ln  28448  mirbtwnhl  28477  colmid  28485  symquadlem  28486  midexlem  28489  ragperp  28514  colperp  28526  midex  28534  oppperpex  28550  hlpasch  28553  colopp  28566  lmieu  28581  lmicom  28585  lmimid  28591  lmiisolem  28593  trgcopy  28601  cgracgr  28615  cgraswap  28617  cgracol  28625  hashecclwwlkn1  29880  xlt2addrd  32522  fprodex01  32582  ssmxidl  33177  lvecdim0  33290  minplyirred  33371  irredminply  33374  zarclssn  33464  esumcvgre  33700  ordtoplem  35909  ordcmp  35921  onsucuni3  36836  dvasin  37166  eqvreldisj  38075  lkrshp4  38569  2at0mat0  38987  trlator0  39633  dia2dimlem2  40527  dia2dimlem3  40528  dochkrshp  40848  dochkrshp4  40851  lcfl6  40962  lclkrlem2k  40979  hdmap14lem6  41335  hgmapval0  41354  sticksstones12a  41613  sticksstones13  41615  acongneg2  42370  unxpwdom3  42491  dflim5  42730  mnuprdlem1  43681  mnurndlem1  43690  disjinfi  44537  xrssre  44702  icccncfext  45247  wallispilem3  45427  fourierdlem93  45559  fourierdlem101  45567  nneop  47571  itsclinecirc0  47818  itsclinecirc0b  47819  itsclinecirc0in  47820  inlinecirc02plem  47831  inlinecirc02p  47832

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »