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

Theorem necomd 2685
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 2683 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 196 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-cleq 2426  df-ne 2598
This theorem is referenced by:  difsnb  4003  0nelop  4569  xpdifid  5254  difsnen  7381  fofinf1o  7580  en2eleq  8163  en2other2  8164  ackbij1lem15  8391  infpssrlem5  8464  fin23lem24  8479  fin23lem31  8500  isf32lem9  8518  canthnumlem  8802  canthp1lem2  8807  npomex  9152  ltned  9497  lt0ne0  9792  recgt0  10160  zneo  10711  xrltne  11124  supxrbnd  11278  seqf1olem1  11828  nn0opthi  12031  hashtpg  12169  hashge3el3dif  12170  cats1un  12353  geoserg  13310  geolim  13312  geolim2  13313  tanadd  13433  ruclem6  13499  ruclem7  13500  isprm5  13780  oddprm  13864  pcmpt  13936  cshwshashlem3  14106  mrissmrcd  14560  pmtrprfv  15938  symggen  15955  dprdcntz  16465  dprdres  16498  ablfac1b  16544  lbspss  17084  lspsnnecom  17121  lspindp2l  17136  lspindp2  17137  islbs3  17157  lbsextlem4  17163  sralem  17179  lidlnz  17231  psrridm  17409  psrridmOLD  17410  coe1tmfv2  17625  coe1tmmul  17627  uvcf1  18058  frlmup2  18068  mdetralt  18255  mdetunilem2  18260  mdetunilem6  18264  mdetunilem7  18265  maducoeval2  18287  madurid  18291  en2top  18431  cmpfi  18852  snfil  19278  tsmsfbas  19539  zcld  20231  iccpnfhmeo  20358  xrhmeo  20359  evth  20372  minveclem3b  20756  i1fres  21024  dvcnvlem  21289  ig1peu  21527  ig1pdvds  21532  aaliou3lem9  21700  taylthlem2  21723  abelthlem2  21781  abelthlem7  21787  tanregt0  21879  logne0  21935  logcj  21939  argimgt0  21945  dvloglem  21977  logf1o2  21979  ang180lem1  22089  ang180lem2  22090  ang180lem3  22091  ang180lem4  22092  ang180lem5  22093  ang180  22094  isosctrlem3  22102  ssscongptld  22104  angpieqvdlem  22107  angpieqvdlem2  22108  angpieqvd  22110  chordthmlem  22111  chordthmlem2  22112  chordthm  22116  asinneg  22165  ppiltx  22399  perfectlem2  22453  lgsneg  22542  lgsqr  22569  lgseisenlem4  22575  lgsquadlem1  22577  lgsquadlem3  22579  lgsquad2  22583  dchrisum0flblem1  22641  tgbtwnouttr  22831  tgifscgr  22841  tgcgrxfr  22850  tglngval  22863  tgfscgr  22875  tgbtwnconn1lem3  22881  tgbtwnconn3  22884  legtrid  22897  lncom  22902  tgisline  22905  tglineeltr  22907  tglineelsb2  22908  tglinecom  22911  tglinethru  22912  ttgcontlem1  22953  cchhllem  22955  brbtwn2  22973  axlowdimlem15  23024  axlowdimlem16  23025  axcontlem8  23039  umgraex  23079  isusgra0  23097  usgra1v  23130  cyclnspth  23339  4cycl4dv  23375  vdgr1a  23398  eupap1  23419  eupath2lem3  23422  staddi  25472  ornglmullt  26127  orngrmullt  26128  orngmullt  26129  ofldlt1  26133  ofldchr  26134  isarchiofld  26137  ordtconlem1  26207  logbrec  26317  cntnevol  26495  sgnmul  26772  sgn0bi  26777  sgnmulsgp  26780  signstfveq0a  26824  signsvfpn  26833  derangenlem  26906  subfacp1lem1  26914  subfacp1lem3  26917  subfacp1lem5  26919  nodenselem3  27670  dfrdg4  27827  ifscgr  27921  cgrxfr  27932  btwnconn1lem8  27971  btwnconn3  27980  segcon2  27982  broutsideof3  28003  outsideoftr  28006  outsideofeq  28007  outsideofeu  28008  lineunray  28024  lineelsb2  28025  linethru  28030  fin2solem  28256  dvtanlem  28282  itg2addnclem2  28285  ftc1cnnc  28307  heibor1lem  28549  maxidln0  28686  jm2.26lem3  29192  rpnnen3lem  29222  rpnnen3  29223  fnchoice  29593  refsum2cnlem1  29601  stoweidlem43  29681  stirlinglem5  29716  stirlinglem7  29718  2spot2iun2spont  30253  usg2cwwk2dif  30337  1to3vfriswmgra  30442  frghash2spot  30499  01eq0rng  30605  lvecpsslmod  30755  chordthmALT  31368  bj-bary1lem  32171  bj-bary1lem1  32172  bj-bary1  32173  lshpnelb  32199  lsatssn0  32217  lsatcv0  32246  lsat0cv  32248  lsatexch1  32261  l1cvat  32270  atlen0  32525  cvlsupr2  32558  atcvrj2b  32646  2atlt  32653  atbtwn  32660  3noncolr2  32663  4noncolr3  32667  3dimlem3  32675  3dimlem3OLDN  32676  3dimlem4  32678  3dimlem4OLDN  32679  3dim2  32682  1cvratex  32687  1cvrat  32690  ps-1  32691  ps-2  32692  hlatexch4  32695  3atlem4  32700  3atlem6  32702  4atlem0ae  32808  4atlem0be  32809  dalemccnedd  32901  dalemrotps  32905  dalem21  32908  dalem23  32910  dalem27  32913  dalem41  32927  dalem44  32930  dalem54  32940  lnatexN  32993  lnjatN  32994  llnexchb2lem  33082  llnexchb2  33083  lhpn0  33218  lhpexle3lem  33225  lhpmatb  33245  4atexlemswapqr  33277  4atexlemc  33283  4atexlemnclw  33284  4atexlemcnd  33286  4atexlemex4  33287  4atexlemex6  33288  4atex  33290  trlat  33383  trlval4  33402  cdlemc5  33409  cdlemd4  33415  cdlemd7  33418  cdlemd9  33420  cdleme0e  33431  cdleme3b  33443  cdleme3c  33444  cdleme3e  33446  cdleme3h  33449  cdleme7aa  33456  cdleme7e  33461  cdleme7ga  33462  cdleme9  33467  cdleme11c  33475  cdleme11e  33477  cdleme11fN  33478  cdleme11h  33480  cdleme11j  33481  cdleme11k  33482  cdleme15b  33489  cdleme15c  33490  cdleme17c  33502  cdleme18b  33506  cdlemesner  33510  cdleme20zN  33515  cdleme19c  33519  cdleme19d  33520  cdleme19e  33521  cdleme20m  33537  cdleme21a  33539  cdleme21b  33540  cdleme21c  33541  cdleme22f2  33561  cdleme28b  33585  cdleme36a  33674  cdleme36m  33675  cdleme41sn4aw  33689  cdleme43bN  33704  cdleme43dN  33706  cdleme46f2g2  33707  cdleme46f2g1  33708  cdleme4gfv  33721  cdlemeg46nlpq  33731  cdlemeg46req  33743  cdlemeg46fgN  33748  cdlemf1  33775  cdlemg8b  33842  cdlemg9a  33846  cdlemg12g  33863  cdlemg12  33864  cdlemg13a  33865  cdlemg17pq  33886  cdlemg18a  33892  cdlemg18c  33894  cdlemg19a  33897  cdlemg19  33898  cdlemg21  33900  cdlemg31b0N  33908  cdlemg31b0a  33909  cdlemg31c  33913  cdlemg33b0  33915  cdlemg33c0  33916  trlcone  33942  cdlemg42  33943  cdlemg44a  33945  cdlemg46  33949  cdlemh1  34029  cdlemh2  34030  cdlemh  34031  cdlemj3  34037  cdlemk3  34047  cdlemki  34055  cdlemksv2  34061  cdlemk12  34064  cdlemk14  34068  cdlemk15  34069  cdlemk7u  34084  cdlemk11u  34085  cdlemk12u  34086  cdlemk21N  34087  cdlemk20  34088  cdlemk22  34107  cdlemk26-3  34120  cdlemk27-3  34121  cdlemk28-3  34122  cdlemkfid3N  34139  cdlemk11ta  34143  cdlemk47  34163  cdlemk54  34172  dia2dimlem1  34279  dochsat  34598  dochshpncl  34599  lclkrlem2b  34723  lcfrlem21  34778  baerlem5amN  34931  baerlem5bmN  34932  baerlem5abmN  34933  mapdindp4  34938  mapdheq2  34944  mapdheq2biN  34945  mapdh6aN  34950  mapdh6dN  34954  mapdh6eN  34955  mapdh6hN  34958  mapdh7eN  34963  mapdh7dN  34965  mapdh7fN  34966  mapdh8ab  34992  mapdh8ad  34994  mapdh8e  34999  mapdh9a  35005  mapdh9aOLDN  35006  hdmap1l6a  35025  hdmap1l6d  35029  hdmap1l6e  35030  hdmap1l6h  35033  hdmap1eulem  35039  hdmap1eulemOLDN  35040  hdmapval0  35051  hdmapeveclem  35052  hdmapval3lemN  35055  hdmap10lem  35057  hdmap11lem1  35059  hdmaprnlem3N  35068  hdmaprnlem9N  35075  hdmaprnlem3eN  35076
  Copyright terms: Public domain W3C validator