MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necomd Structured version   Unicode version

Theorem necomd 2725
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necomd  |-  ( ph  ->  B  =/=  A )

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 necom 2723 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 196 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2651
This theorem is referenced by:  difsnb  4158  0nelop  4726  xpdifid  5420  difsnen  7592  fofinf1o  7793  en2eleq  8377  en2other2  8378  ackbij1lem15  8605  infpssrlem5  8678  fin23lem24  8693  fin23lem31  8714  isf32lem9  8732  canthnumlem  9015  canthp1lem2  9020  npomex  9363  ltned  9710  lt0ne0  10014  recgt0  10382  zneo  10941  xrltne  11369  supxrbnd  11523  seqf1olem1  12131  nn0opthi  12335  hashtpg  12510  hashge3el3dif  12511  cats1un  12695  geoserg  13762  geolim  13764  geolim2  13765  tanadd  13987  ruclem6  14055  ruclem7  14056  isprm5  14340  oddprm  14426  pcmpt  14498  cshwshashlem3  14669  mrissmrcd  15132  estrres  15610  pmtrprfv  16680  symggen  16697  dprdcntz  17239  dprdres  17273  ablfac1b  17319  lbspss  17926  lspsnnecom  17963  lspindp2l  17978  lspindp2  17979  islbs3  17999  lbsextlem4  18005  sralem  18021  lidlnz  18074  01eq0ring  18118  psrridm  18256  psrridmOLD  18257  coe1tmfv2  18514  coe1tmmul  18516  uvcf1  18997  frlmup2  19004  dmatmul  19169  mdetralt  19280  mdetunilem2  19285  mdetunilem6  19289  mdetunilem7  19290  maducoeval2  19312  madurid  19316  fvmptnn04ifa  19521  en2top  19657  cmpfi  20078  snfil  20534  tsmsfbas  20795  zcld  21487  iccpnfhmeo  21614  xrhmeo  21615  evth  21628  minveclem3b  22012  i1fres  22281  dvcnvlem  22546  ig1peu  22741  ig1pdvds  22746  aaliou3lem9  22915  taylthlem2  22938  abelthlem2  22996  abelthlem7  23002  tanregt0  23095  logcj  23162  argimgt0  23168  dvloglem  23200  logf1o2  23202  logbrec  23324  ang180lem1  23343  ang180lem2  23344  ang180lem3  23345  ang180lem4  23346  ang180lem5  23347  ang180  23348  isosctrlem3  23354  ssscongptld  23356  angpieqvdlem  23359  angpieqvdlem2  23360  angpieqvd  23362  chordthmlem  23363  chordthmlem2  23364  chordthm  23368  asinneg  23417  ppiltx  23652  perfectlem2  23706  lgsneg  23795  lgsqr  23822  lgseisenlem4  23828  lgsquadlem1  23830  lgsquadlem3  23832  lgsquad2  23836  dchrisum0flblem1  23894  tgbtwnouttr  24092  tgifscgr  24104  tgcgrxfr  24113  tglngval  24142  tgfscgr  24159  tgbtwnconn1lem3  24165  tgbtwnconn3  24168  legtrid  24182  hltr  24198  hlbtwn  24199  btwnhl1  24200  btwnhl  24202  lncom  24206  tgisline  24211  tglineeltr  24215  tglineelsb2  24216  tglinecom  24219  tglinethru  24220  ncolncol  24230  coltr  24231  coltr2  24232  coltr3  24233  symquadlem  24270  midexlem  24273  ragcol  24280  ragcgr  24288  perpneq  24295  footex  24299  foot  24300  footne  24301  colperpexlem3  24310  mideulem2  24312  opphllem  24313  midex  24315  opphllem1  24323  opphllem2  24324  opphllem3  24325  opphllem4  24326  opphllem5  24327  opphllem6  24328  lnopp2hpgb  24336  lmieu  24354  hypcgrlem1  24368  hypcgrlem2  24369  cgraid  24374  ttgcontlem1  24393  cchhllem  24395  brbtwn2  24413  axlowdimlem15  24464  axlowdimlem16  24465  axcontlem8  24479  umgraex  24528  isusgra0  24552  usgraop  24555  usgra1v  24595  cyclnspth  24836  4cycl4dv  24872  usg2cwwk2dif  25025  2spot2iun2spont  25096  vdgr1a  25111  eupap1  25181  eupath2lem3  25184  1to3vfriswmgra  25212  frghash2spot  25268  staddi  27366  ornglmullt  28035  orngrmullt  28036  orngmullt  28037  ofldlt1  28041  ofldchr  28042  isarchiofld  28045  ordtconlem1  28144  esumrnmpt2  28300  cntnevol  28439  signstfveq0a  28800  derangenlem  28882  subfacp1lem1  28890  subfacp1lem3  28893  subfacp1lem5  28895  nodenselem3  29686  dfrdg4  29831  ifscgr  29925  cgrxfr  29936  btwnconn1lem8  29975  btwnconn3  29984  segcon2  29986  broutsideof3  30007  outsideoftr  30010  outsideofeq  30011  outsideofeu  30012  lineunray  30028  lineelsb2  30029  linethru  30034  fin2solem  30282  dvtanlem  30307  itg2addnclem2  30310  ftc1cnnc  30332  heibor1lem  30548  maxidln0  30685  jm2.26lem3  31185  rpnnen3lem  31215  rpnnen3  31216  bcc0  31489  fnchoice  31647  refsum2cnlem1  31655  flltnz  31740  icoiccdif  31806  limcresiooub  31890  limcleqr  31892  limclner  31899  icccncfext  31932  cncfiooiccre  31940  dvnxpaek  31981  stoweidlem43  32067  stirlinglem5  32102  stirlinglem7  32104  dirkercncflem1  32127  fourierdlem24  32155  fourierdlem32  32163  fourierdlem33  32164  fourierdlem34  32165  fourierdlem35  32166  fourierdlem46  32177  fourierdlem48  32179  fourierdlem49  32180  fourierdlem64  32195  fourierdlem65  32196  fourierdlem74  32205  fourierdlem76  32207  fourierdlem79  32210  fourierdlem81  32212  fourierdlem91  32222  fourierdlem102  32233  fourierdlem114  32245  etransclem15  32274  etransclem24  32283  perfectALTVlem2  32616  usgvad2edg  32802  nnsgrpnmnd  32897  nrhmzr  32952  lvecpsslmod  33381  chordthmALT  34153  bj-bary1lem  35095  bj-bary1lem1  35096  bj-bary1  35097  lshpnelb  35125  lsatssn0  35143  lsatcv0  35172  lsat0cv  35174  lsatexch1  35187  l1cvat  35196  atlen0  35451  cvlsupr2  35484  atcvrj2b  35572  2atlt  35579  atbtwn  35586  3noncolr2  35589  4noncolr3  35593  3dimlem3  35601  3dimlem3OLDN  35602  3dimlem4  35604  3dimlem4OLDN  35605  3dim2  35608  1cvratex  35613  1cvrat  35616  ps-1  35617  ps-2  35618  hlatexch4  35621  3atlem4  35626  3atlem6  35628  4atlem0ae  35734  4atlem0be  35735  dalemccnedd  35827  dalemrotps  35831  dalem21  35834  dalem23  35836  dalem27  35839  dalem41  35853  dalem44  35856  dalem54  35866  lnatexN  35919  lnjatN  35920  llnexchb2lem  36008  llnexchb2  36009  lhpn0  36144  lhpexle3lem  36151  lhpmatb  36171  4atexlemswapqr  36203  4atexlemc  36209  4atexlemnclw  36210  4atexlemcnd  36212  4atexlemex4  36213  4atexlemex6  36214  4atex  36216  trlat  36310  trlval4  36329  cdlemc5  36336  cdlemd4  36342  cdlemd7  36345  cdlemd9  36347  cdleme0e  36358  cdleme3b  36370  cdleme3c  36371  cdleme3e  36373  cdleme3h  36376  cdleme7aa  36383  cdleme7e  36388  cdleme7ga  36389  cdleme9  36394  cdleme11c  36402  cdleme11e  36404  cdleme11fN  36405  cdleme11h  36407  cdleme11j  36408  cdleme11k  36409  cdleme15b  36416  cdleme15c  36417  cdleme17c  36429  cdleme18b  36433  cdlemesner  36437  cdleme20zN  36442  cdleme19c  36447  cdleme19d  36448  cdleme19e  36449  cdleme20m  36465  cdleme21a  36467  cdleme21b  36468  cdleme21c  36469  cdleme22f2  36489  cdleme28b  36513  cdleme36a  36602  cdleme36m  36603  cdleme41sn4aw  36617  cdleme43bN  36632  cdleme43dN  36634  cdleme46f2g2  36635  cdleme46f2g1  36636  cdleme4gfv  36649  cdlemeg46nlpq  36659  cdlemeg46req  36671  cdlemeg46fgN  36676  cdlemf1  36703  cdlemg8b  36770  cdlemg9a  36774  cdlemg12g  36791  cdlemg12  36792  cdlemg13a  36793  cdlemg17pq  36814  cdlemg18a  36820  cdlemg18c  36822  cdlemg19a  36825  cdlemg19  36826  cdlemg21  36828  cdlemg31b0N  36836  cdlemg31b0a  36837  cdlemg31c  36841  cdlemg33b0  36843  cdlemg33c0  36844  trlcone  36870  cdlemg42  36871  cdlemg44a  36873  cdlemg46  36877  cdlemh1  36957  cdlemh2  36958  cdlemh  36959  cdlemj3  36965  cdlemk3  36975  cdlemki  36983  cdlemksv2  36989  cdlemk12  36992  cdlemk14  36996  cdlemk15  36997  cdlemk7u  37012  cdlemk11u  37013  cdlemk12u  37014  cdlemk21N  37015  cdlemk20  37016  cdlemk22  37035  cdlemk26-3  37048  cdlemk27-3  37049  cdlemk28-3  37050  cdlemkfid3N  37067  cdlemk11ta  37071  cdlemk47  37091  cdlemk54  37100  dia2dimlem1  37207  dochsat  37526  dochshpncl  37527  lclkrlem2b  37651  lcfrlem21  37706  baerlem5amN  37859  baerlem5bmN  37860  baerlem5abmN  37861  mapdindp4  37866  mapdheq2  37872  mapdheq2biN  37873  mapdh6aN  37878  mapdh6dN  37882  mapdh6eN  37883  mapdh6hN  37886  mapdh7eN  37891  mapdh7dN  37893  mapdh7fN  37894  mapdh8ab  37920  mapdh8ad  37922  mapdh8e  37927  mapdh9a  37933  mapdh9aOLDN  37934  hdmap1l6a  37953  hdmap1l6d  37957  hdmap1l6e  37958  hdmap1l6h  37961  hdmap1eulem  37967  hdmap1eulemOLDN  37968  hdmapval0  37979  hdmapeveclem  37980  hdmapval3lemN  37983  hdmap10lem  37985  hdmap11lem1  37987  hdmaprnlem3N  37996  hdmaprnlem9N  38003  hdmaprnlem3eN  38004  imo72b2lem0  38495  imo72b2lem2  38497  imo72b2lem1  38501  imo72b2  38506
  Copyright terms: Public domain W3C validator