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

Theorem necomd 2738
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 2736 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 196 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  difsnb  4169  0nelop  4737  xpdifid  5435  difsnen  7599  fofinf1o  7801  en2eleq  8386  en2other2  8387  ackbij1lem15  8614  infpssrlem5  8687  fin23lem24  8702  fin23lem31  8723  isf32lem9  8741  canthnumlem  9026  canthp1lem2  9031  npomex  9374  ltned  9720  lt0ne0  10018  recgt0  10386  zneo  10943  xrltne  11366  supxrbnd  11520  seqf1olem1  12114  nn0opthi  12318  hashtpg  12489  hashge3el3dif  12490  cats1un  12664  geoserg  13640  geolim  13642  geolim2  13643  tanadd  13763  ruclem6  13829  ruclem7  13830  isprm5  14112  oddprm  14198  pcmpt  14270  cshwshashlem3  14440  mrissmrcd  14895  pmtrprfv  16284  symggen  16301  dprdcntz  16844  dprdres  16877  ablfac1b  16923  lbspss  17528  lspsnnecom  17565  lspindp2l  17580  lspindp2  17581  islbs3  17601  lbsextlem4  17607  sralem  17623  lidlnz  17675  01eq0rng  17719  psrridm  17857  psrridmOLD  17858  coe1tmfv2  18115  coe1tmmul  18117  uvcf1  18618  frlmup2  18628  dmatmul  18794  mdetralt  18905  mdetunilem2  18910  mdetunilem6  18914  mdetunilem7  18915  maducoeval2  18937  madurid  18941  fvmptnn04ifa  19146  en2top  19281  cmpfi  19702  snfil  20128  tsmsfbas  20389  zcld  21081  iccpnfhmeo  21208  xrhmeo  21209  evth  21222  minveclem3b  21606  i1fres  21875  dvcnvlem  22140  ig1peu  22335  ig1pdvds  22340  aaliou3lem9  22508  taylthlem2  22531  abelthlem2  22589  abelthlem7  22595  tanregt0  22687  logne0  22743  logcj  22747  argimgt0  22753  dvloglem  22785  logf1o2  22787  ang180lem1  22897  ang180lem2  22898  ang180lem3  22899  ang180lem4  22900  ang180lem5  22901  ang180  22902  isosctrlem3  22910  ssscongptld  22912  angpieqvdlem  22915  angpieqvdlem2  22916  angpieqvd  22918  chordthmlem  22919  chordthmlem2  22920  chordthm  22924  asinneg  22973  ppiltx  23207  perfectlem2  23261  lgsneg  23350  lgsqr  23377  lgseisenlem4  23383  lgsquadlem1  23385  lgsquadlem3  23387  lgsquad2  23391  dchrisum0flblem1  23449  tgbtwnouttr  23644  tgifscgr  23656  tgcgrxfr  23665  tglngval  23694  tgfscgr  23710  tgbtwnconn1lem3  23716  tgbtwnconn3  23719  legtrid  23733  lncom  23744  tgisline  23749  tglineeltr  23753  tglineelsb2  23754  tglinecom  23757  tglinethru  23758  ncolncol  23767  coltr  23768  coltr2  23769  coltr3  23770  symquadlem  23802  midexlem  23805  ragcol  23812  ragcgr  23820  perpneq  23827  footex  23831  foot  23832  colperpexlem3  23839  mideulem  23841  mideu  23842  lmieu  23855  hypcgrlem1  23869  hypcgrlem2  23870  ttgcontlem1  23892  cchhllem  23894  brbtwn2  23912  axlowdimlem15  23963  axlowdimlem16  23964  axcontlem8  23978  umgraex  24027  isusgra0  24051  usgraop  24054  usgra1v  24094  cyclnspth  24335  4cycl4dv  24371  usg2cwwk2dif  24524  2spot2iun2spont  24595  vdgr1a  24610  eupap1  24680  eupath2lem3  24683  1to3vfriswmgra  24711  frghash2spot  24768  staddi  26869  ornglmullt  27488  orngrmullt  27489  orngmullt  27490  ofldlt1  27494  ofldchr  27495  isarchiofld  27498  ordtconlem1  27570  logbrec  27689  cntnevol  27867  sgnmul  28149  sgn0bi  28154  sgnmulsgp  28157  signstfveq0a  28201  signsvfpn  28210  derangenlem  28283  subfacp1lem1  28291  subfacp1lem3  28294  subfacp1lem5  28296  nodenselem3  29048  dfrdg4  29205  ifscgr  29299  cgrxfr  29310  btwnconn1lem8  29349  btwnconn3  29358  segcon2  29360  broutsideof3  29381  outsideoftr  29384  outsideofeq  29385  outsideofeu  29386  lineunray  29402  lineelsb2  29403  linethru  29408  fin2solem  29644  dvtanlem  29669  itg2addnclem2  29672  ftc1cnnc  29694  heibor1lem  29936  maxidln0  30073  jm2.26lem3  30575  rpnnen3lem  30605  rpnnen3  30606  fnchoice  31010  refsum2cnlem1  31018  flltnz  31103  icoiccdif  31156  limcresiooub  31212  limcleqr  31214  limclner  31221  icccncfext  31254  cncfiooicclem1  31260  cncfiooiccre  31262  ditgeqiooicc  31306  itgioocnicc  31323  iblcncfioo  31324  stoweidlem43  31371  stirlinglem5  31406  stirlinglem7  31408  dirkercncflem1  31431  fourierdlem24  31459  fourierdlem32  31467  fourierdlem33  31468  fourierdlem34  31469  fourierdlem35  31470  fourierdlem42  31477  fourierdlem46  31481  fourierdlem48  31483  fourierdlem49  31484  fourierdlem64  31499  fourierdlem65  31500  fourierdlem74  31509  fourierdlem76  31511  fourierdlem79  31514  fourierdlem81  31516  fourierdlem82  31517  fourierdlem91  31526  fourierdlem102  31537  fourierdlem114  31549  usgvad2edg  31906  lvecpsslmod  32207  chordthmALT  32831  bj-bary1lem  33769  bj-bary1lem1  33770  bj-bary1  33771  lshpnelb  33799  lsatssn0  33817  lsatcv0  33846  lsat0cv  33848  lsatexch1  33861  l1cvat  33870  atlen0  34125  cvlsupr2  34158  atcvrj2b  34246  2atlt  34253  atbtwn  34260  3noncolr2  34263  4noncolr3  34267  3dimlem3  34275  3dimlem3OLDN  34276  3dimlem4  34278  3dimlem4OLDN  34279  3dim2  34282  1cvratex  34287  1cvrat  34290  ps-1  34291  ps-2  34292  hlatexch4  34295  3atlem4  34300  3atlem6  34302  4atlem0ae  34408  4atlem0be  34409  dalemccnedd  34501  dalemrotps  34505  dalem21  34508  dalem23  34510  dalem27  34513  dalem41  34527  dalem44  34530  dalem54  34540  lnatexN  34593  lnjatN  34594  llnexchb2lem  34682  llnexchb2  34683  lhpn0  34818  lhpexle3lem  34825  lhpmatb  34845  4atexlemswapqr  34877  4atexlemc  34883  4atexlemnclw  34884  4atexlemcnd  34886  4atexlemex4  34887  4atexlemex6  34888  4atex  34890  trlat  34983  trlval4  35002  cdlemc5  35009  cdlemd4  35015  cdlemd7  35018  cdlemd9  35020  cdleme0e  35031  cdleme3b  35043  cdleme3c  35044  cdleme3e  35046  cdleme3h  35049  cdleme7aa  35056  cdleme7e  35061  cdleme7ga  35062  cdleme9  35067  cdleme11c  35075  cdleme11e  35077  cdleme11fN  35078  cdleme11h  35080  cdleme11j  35081  cdleme11k  35082  cdleme15b  35089  cdleme15c  35090  cdleme17c  35102  cdleme18b  35106  cdlemesner  35110  cdleme20zN  35115  cdleme19c  35119  cdleme19d  35120  cdleme19e  35121  cdleme20m  35137  cdleme21a  35139  cdleme21b  35140  cdleme21c  35141  cdleme22f2  35161  cdleme28b  35185  cdleme36a  35274  cdleme36m  35275  cdleme41sn4aw  35289  cdleme43bN  35304  cdleme43dN  35306  cdleme46f2g2  35307  cdleme46f2g1  35308  cdleme4gfv  35321  cdlemeg46nlpq  35331  cdlemeg46req  35343  cdlemeg46fgN  35348  cdlemf1  35375  cdlemg8b  35442  cdlemg9a  35446  cdlemg12g  35463  cdlemg12  35464  cdlemg13a  35465  cdlemg17pq  35486  cdlemg18a  35492  cdlemg18c  35494  cdlemg19a  35497  cdlemg19  35498  cdlemg21  35500  cdlemg31b0N  35508  cdlemg31b0a  35509  cdlemg31c  35513  cdlemg33b0  35515  cdlemg33c0  35516  trlcone  35542  cdlemg42  35543  cdlemg44a  35545  cdlemg46  35549  cdlemh1  35629  cdlemh2  35630  cdlemh  35631  cdlemj3  35637  cdlemk3  35647  cdlemki  35655  cdlemksv2  35661  cdlemk12  35664  cdlemk14  35668  cdlemk15  35669  cdlemk7u  35684  cdlemk11u  35685  cdlemk12u  35686  cdlemk21N  35687  cdlemk20  35688  cdlemk22  35707  cdlemk26-3  35720  cdlemk27-3  35721  cdlemk28-3  35722  cdlemkfid3N  35739  cdlemk11ta  35743  cdlemk47  35763  cdlemk54  35772  dia2dimlem1  35879  dochsat  36198  dochshpncl  36199  lclkrlem2b  36323  lcfrlem21  36378  baerlem5amN  36531  baerlem5bmN  36532  baerlem5abmN  36533  mapdindp4  36538  mapdheq2  36544  mapdheq2biN  36545  mapdh6aN  36550  mapdh6dN  36554  mapdh6eN  36555  mapdh6hN  36558  mapdh7eN  36563  mapdh7dN  36565  mapdh7fN  36566  mapdh8ab  36592  mapdh8ad  36594  mapdh8e  36599  mapdh9a  36605  mapdh9aOLDN  36606  hdmap1l6a  36625  hdmap1l6d  36629  hdmap1l6e  36630  hdmap1l6h  36633  hdmap1eulem  36639  hdmap1eulemOLDN  36640  hdmapval0  36651  hdmapeveclem  36652  hdmapval3lemN  36655  hdmap10lem  36657  hdmap11lem1  36659  hdmaprnlem3N  36668  hdmaprnlem9N  36675  hdmaprnlem3eN  36676
  Copyright terms: Public domain W3C validator