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

Theorem necomd 2702
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 2700 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 199 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-ne 2627
This theorem is referenced by:  difsnb  4145  0nelop  4711  xpdifid  5285  difsnen  7660  fofinf1o  7858  en2eleq  8438  en2other2  8439  ackbij1lem15  8662  infpssrlem5  8735  fin23lem24  8750  fin23lem31  8771  isf32lem9  8789  canthnumlem  9072  canthp1lem2  9077  npomex  9420  ltned  9770  lt0ne0  10079  recgt0  10448  zneo  11018  xrltne  11460  supxrbnd  11614  seqf1olem1  12249  nn0opthi  12453  hashtpg  12632  hashge3el3dif  12633  cats1un  12817  sumtp  13788  geoserg  13902  geolim  13904  geolim2  13905  tanadd  14199  ruclem6  14265  ruclem7  14266  isprm5  14622  oddprm  14728  pcmpt  14800  cshwshashlem3  15031  mrissmrcd  15497  estrres  15975  pmtrprfv  17045  symggen  17062  dprdcntz  17575  dprdres  17596  ablfac1b  17638  lbspss  18240  lspsnnecom  18277  lspindp2l  18292  lspindp2  18293  islbs3  18313  lbsextlem4  18319  sralem  18335  lidlnz  18387  01eq0ring  18431  psrridm  18563  coe1tmfv2  18803  coe1tmmul  18805  uvcf1  19281  frlmup2  19288  dmatmul  19453  mdetralt  19564  mdetunilem2  19569  mdetunilem6  19573  mdetunilem7  19574  maducoeval2  19596  madurid  19600  fvmptnn04ifa  19805  en2top  19932  cmpfi  20354  snfil  20810  tsmsfbas  21073  zcld  21742  iccpnfhmeo  21869  xrhmeo  21870  evth  21883  minveclem3b  22263  i1fres  22540  dvcnvlem  22805  ig1peu  22997  ig1pdvds  23002  aaliou3lem9  23171  taylthlem2  23194  abelthlem2  23252  abelthlem7  23258  tanregt0  23353  logcj  23420  argimgt0  23426  dvloglem  23458  logf1o2  23460  logbrec  23584  ang180lem1  23603  ang180lem2  23604  ang180lem3  23605  ang180lem4  23606  ang180lem5  23607  ang180  23608  isosctrlem3  23614  ssscongptld  23616  angpieqvdlem  23619  angpieqvdlem2  23620  angpieqvd  23622  chordthmlem  23623  chordthmlem2  23624  chordthm  23628  asinneg  23677  ppiltx  23967  perfectlem2  24021  lgsneg  24110  lgsqr  24137  lgseisenlem4  24143  lgsquadlem1  24145  lgsquadlem3  24147  lgsquad2  24151  dchrisum0flblem1  24209  tgbtwnouttr  24404  tgifscgr  24416  tgcgrxfr  24425  tglngval  24456  tgfscgr  24473  tgbtwnconn1lem3  24479  tgbtwnconn3  24482  legtrid  24496  hltr  24515  hlbtwn  24516  btwnhl1  24517  btwnhl  24519  hlcgrex  24520  hlcgreulem  24521  lncom  24526  tgisline  24531  tglineeltr  24535  tglineelsb2  24536  tglinecom  24539  tglinethru  24540  ncolncol  24550  coltr  24551  coltr2  24552  coltr3  24553  symquadlem  24591  midexlem  24594  ragcol  24601  ragcgr  24609  perpneq  24616  footex  24620  foot  24621  footne  24622  colperpexlem3  24631  mideulem2  24633  opphllem  24634  midex  24636  opphllem1  24646  opphllem2  24647  opphllem3  24648  opphllem4  24649  opphllem5  24650  opphllem6  24651  outpasch  24654  lnopp2hpgb  24661  colhp  24668  lmieu  24682  hypcgrlem1  24697  hypcgrlem2  24698  lnperpex  24701  trgcopy  24702  trgcopyeulem  24703  iscgra1  24708  cgrane2  24711  cgrane3  24712  cgrane4  24713  cgracgr  24716  cgraid  24717  cgraswap  24718  cgrcgra  24719  cgracom  24720  cgratr  24721  cgracol  24724  dfcgra2  24726  acopy  24727  acopyeu  24728  tgsas1  24734  tgsas2  24736  tgasa1  24738  tgsss1  24740  ttgcontlem1  24761  cchhllem  24763  brbtwn2  24781  axlowdimlem15  24832  axlowdimlem16  24833  axcontlem8  24847  umgraex  24896  isusgra0  24920  usgraop  24923  usgra1v  24963  cyclnspth  25204  4cycl4dv  25240  usg2cwwk2dif  25393  2spot2iun2spont  25464  vdgr1a  25479  eupap1  25549  eupath2lem3  25552  1to3vfriswmgra  25580  frghash2spot  25636  staddi  27734  ornglmullt  28409  orngrmullt  28410  orngmullt  28411  ofldlt1  28415  ofldchr  28416  isarchiofld  28419  psgnfzto1stlem  28452  1smat1  28469  submateqlem1  28472  madjusmdetlem2  28493  ordtconlem1  28569  esumrnmpt2  28728  cntnevol  28889  signstfveq0a  29253  derangenlem  29682  subfacp1lem1  29690  subfacp1lem3  29693  subfacp1lem5  29695  nodenselem3  30357  dfrdg4  30503  ifscgr  30596  cgrxfr  30607  btwnconn1lem8  30646  btwnconn3  30655  segcon2  30657  broutsideof3  30678  outsideoftr  30681  outsideofeq  30682  outsideofeu  30683  lineunray  30699  lineelsb2  30700  linethru  30705  bj-bary1lem  31460  bj-bary1lem1  31461  bj-bary1  31462  fin2solem  31634  poimirlem9  31652  poimirlem15  31658  poimirlem20  31663  poimirlem24  31667  poimirlem25  31668  poimirlem27  31670  dvtanlemOLD  31694  itg2addnclem2  31697  ftc1cnnc  31719  heibor1lem  31844  maxidln0  31981  lshpnelb  32258  lsatssn0  32276  lsatcv0  32305  lsat0cv  32307  lsatexch1  32320  l1cvat  32329  atlen0  32584  cvlsupr2  32617  atcvrj2b  32705  2atlt  32712  atbtwn  32719  3noncolr2  32722  4noncolr3  32726  3dimlem3  32734  3dimlem3OLDN  32735  3dimlem4  32737  3dimlem4OLDN  32738  3dim2  32741  1cvratex  32746  1cvrat  32749  ps-1  32750  ps-2  32751  hlatexch4  32754  3atlem4  32759  3atlem6  32761  4atlem0ae  32867  4atlem0be  32868  dalemccnedd  32960  dalemrotps  32964  dalem21  32967  dalem23  32969  dalem27  32972  dalem41  32986  dalem44  32989  dalem54  32999  lnatexN  33052  lnjatN  33053  llnexchb2lem  33141  llnexchb2  33142  lhpn0  33277  lhpexle3lem  33284  lhpmatb  33304  4atexlemswapqr  33336  4atexlemc  33342  4atexlemnclw  33343  4atexlemcnd  33345  4atexlemex4  33346  4atexlemex6  33347  4atex  33349  trlat  33443  trlval4  33462  cdlemc5  33469  cdlemd4  33475  cdlemd7  33478  cdlemd9  33480  cdleme0e  33491  cdleme3b  33503  cdleme3c  33504  cdleme3e  33506  cdleme3h  33509  cdleme7aa  33516  cdleme7e  33521  cdleme7ga  33522  cdleme9  33527  cdleme11c  33535  cdleme11e  33537  cdleme11fN  33538  cdleme11h  33540  cdleme11j  33541  cdleme11k  33542  cdleme15b  33549  cdleme15c  33550  cdleme17c  33562  cdleme18b  33566  cdlemesner  33570  cdleme20zN  33575  cdleme19c  33580  cdleme19d  33581  cdleme19e  33582  cdleme20m  33598  cdleme21a  33600  cdleme21b  33601  cdleme21c  33602  cdleme22f2  33622  cdleme28b  33646  cdleme36a  33735  cdleme36m  33736  cdleme41sn4aw  33750  cdleme43bN  33765  cdleme43dN  33767  cdleme46f2g2  33768  cdleme46f2g1  33769  cdleme4gfv  33782  cdlemeg46nlpq  33792  cdlemeg46req  33804  cdlemeg46fgN  33809  cdlemf1  33836  cdlemg8b  33903  cdlemg9a  33907  cdlemg12g  33924  cdlemg12  33925  cdlemg13a  33926  cdlemg17pq  33947  cdlemg18a  33953  cdlemg18c  33955  cdlemg19a  33958  cdlemg19  33959  cdlemg21  33961  cdlemg31b0N  33969  cdlemg31b0a  33970  cdlemg31c  33974  cdlemg33b0  33976  cdlemg33c0  33977  trlcone  34003  cdlemg42  34004  cdlemg44a  34006  cdlemg46  34010  cdlemh1  34090  cdlemh2  34091  cdlemh  34092  cdlemj3  34098  cdlemk3  34108  cdlemki  34116  cdlemksv2  34122  cdlemk12  34125  cdlemk14  34129  cdlemk15  34130  cdlemk7u  34145  cdlemk11u  34146  cdlemk12u  34147  cdlemk21N  34148  cdlemk20  34149  cdlemk22  34168  cdlemk26-3  34181  cdlemk27-3  34182  cdlemk28-3  34183  cdlemkfid3N  34200  cdlemk11ta  34204  cdlemk47  34224  cdlemk54  34233  dia2dimlem1  34340  dochsat  34659  dochshpncl  34660  lclkrlem2b  34784  lcfrlem21  34839  baerlem5amN  34992  baerlem5bmN  34993  baerlem5abmN  34994  mapdindp4  34999  mapdheq2  35005  mapdheq2biN  35006  mapdh6aN  35011  mapdh6dN  35015  mapdh6eN  35016  mapdh6hN  35019  mapdh7eN  35024  mapdh7dN  35026  mapdh7fN  35027  mapdh8ab  35053  mapdh8ad  35055  mapdh8e  35060  mapdh9a  35066  mapdh9aOLDN  35067  hdmap1l6a  35086  hdmap1l6d  35090  hdmap1l6e  35091  hdmap1l6h  35094  hdmap1eulem  35100  hdmap1eulemOLDN  35101  hdmapval0  35112  hdmapeveclem  35113  hdmapval3lemN  35116  hdmap10lem  35118  hdmap11lem1  35120  hdmaprnlem3N  35129  hdmaprnlem9N  35136  hdmaprnlem3eN  35137  jm2.26lem3  35561  rpnnen3lem  35591  rpnnen3  35592  imo72b2lem0  36244  imo72b2lem2  36246  imo72b2lem1  36250  imo72b2  36255  bcc0  36325  chordthmALT  36969  fnchoice  36989  refsum2cnlem1  36997  flltnz  37124  xrleneltd  37154  icoiccdif  37209  limcresiooub  37294  limcleqr  37296  limclner  37303  icccncfext  37336  cncfiooiccre  37344  dvnxpaek  37385  stoweidlem43  37472  stirlinglem5  37508  stirlinglem7  37510  dirkercncflem1  37533  fourierdlem24  37561  fourierdlem32  37569  fourierdlem33  37570  fourierdlem34  37571  fourierdlem35  37572  fourierdlem46  37583  fourierdlem48  37585  fourierdlem49  37586  fourierdlem64  37601  fourierdlem65  37602  fourierdlem74  37611  fourierdlem76  37613  fourierdlem79  37616  fourierdlem81  37618  fourierdlem91  37628  fourierdlem102  37639  fourierdlem114  37651  etransclem15  37680  etransclem24  37689  perfectALTVlem2  38233  usgvad2edg  38480  nnsgrpnmnd  38575  nrhmzr  38630  lvecpsslmod  39059
  Copyright terms: Public domain W3C validator