Theorem necomd 3010

Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)

Hypothesis

Ref	Expression
necomd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
necomd	⊢ (𝜑 → 𝐵 ≠ 𝐴)

Proof of Theorem necomd

Step	Hyp	Ref	Expression
1		necomd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		necom 3008	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

This proof depends on syntax axioms:   → wi 4   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  difsnb  4768  0nelop  5465  xpdifid  6154  f1ounsn  7268  resf1extb  7929  difsnen  9056  fofinf1o  9299  en2eleq  10058  en2other2  10059  ackbij1lem15  10282  infpssrlem5  10356  fin23lem24  10371  fin23lem31  10392  isf32lem9  10410  canthnumlem  10704  canthp1lem2  10709  npomex  11052  ltned  11417  lt0ne0  11751  recgt0  12132  zneo  12751  xrltne  13261  supxrbnd  13427  flltnz  13919  seqf1olem1  14152  nn0opthi  14381  hashtpg  14597  hash7g  14598  hashge3el3dif  14599  cats1un  14837  sumtp  15882  geoserg  16002  geolim  16006  geolim2  16007  tanadd  16302  ruclem6  16370  ruclem7  16371  isprm2lem  16818  isprm5  16845  oddprm  16949  pcmpt  17031  cshwshashlem3  17236  resshom  17550  ressco  17551  mrissmrcd  17775  rescco  17968  estrres  18274  chnccat  18761  chnrev  18762  chnpof1  18765  smndex2dnrinv  19075  pmtrprfv  19628  symggen  19645  dprdcntz  20185  dprdres  20205  ablfac1b  20247  01eq0ringOLD  20743  nrhmzr  20750  zrdrng  20987  ornglmullt  21087  orngrmullt  21088  orngmullt  21089  ofldlt1  21093  lbspss  21318  lspsnnecom  21358  lspindp2l  21373  lspindp2  21374  islbs3  21394  lbsextlem4  21400  lidlnz  21491  isfieldidl  21501  qsidomlem2  21598  ssdifidlprm  21603  ofldchr  21843  uvcf1  22059  frlmup2  22066  psrridm  22231  coe1tmfv2  22555  coe1tmmul  22557  dmatmul  22773  mdetralt  22884  mdetunilem2  22889  mdetunilem6  22893  mdetunilem7  22894  maducoeval2  22916  madurid  22920  fvmptnn04ifa  23129  en2top  23264  cmpfi  23687  snfil  24144  tsmsfbas  24408  zcld  25094  iccpnfhmeo  25227  xrhmeo  25228  evth  25241  minveclem3b  25710  i1fres  25987  dvcnvlem  26257  ig1peu  26454  ig1pdvds  26459  aaliou3lem9  26640  taylthlem2  26664  abelthlem2  26722  abelthlem7  26728  cos02pilt1  26817  tanregt0  26830  logcj  26897  argimgt0  26903  dvloglem  26939  logf1o2  26941  logbrec  27073  ang180lem1  27100  ang180lem2  27101  ang180lem3  27102  ang180lem4  27103  ang180lem5  27104  ang180  27105  isosctrlem3  27111  ssscongptld  27113  affineequivne  27118  angpieqvdlem  27119  angpieqvdlem2  27120  angpieqvd  27122  chordthmlem  27123  chordthmlem2  27124  chordthm  27128  asinneg  27177  ppiltx  27467  perfectlem2  27520  lgsneg  27611  lgsqr  27641  lgseisenlem4  27668  lgsquadlem1  27670  lgsquadlem3  27672  lgsquad2  27676  2lgsoddprm  27706  dchrisum0flblem1  27798  noseponlem  27954  nosep1o  27971  nosep2o  27972  nosupbnd2lem1  28005  noinfbnd2lem1  28020  noetasuplem4  28026  noetainflem4  28030  lesrec  28118  0elright  28231  tgbtwnouttr  28893  tgifscgr  28904  tgcgrxfr  28914  tglngval  28947  tgfscgr  28964  tgbtwnconn1lem3  28970  tgbtwnconn3  28973  legtrid  28987  hltr  29009  hlbtwn  29010  btwnhl1  29011  btwnhl  29013  hlcgrex  29015  hlcgreulem  29016  lncom  29023  tgisline  29028  tglineeltr  29032  tglineelsb2  29033  tglinecom  29036  tglinethru  29037  ncolncol  29048  coltr  29049  coltr3  29050  tglnpt3  29055  tglnpt4  29056  symquadlem  29094  midexlem  29097  mirlni  29100  ragcol  29107  ragcgr  29115  perpneq  29122  footexALT  29126  footexlem1  29127  footexlem2  29128  foot  29130  footne  29131  colperpexlem3  29141  mideulem2  29143  opphllem  29144  midex  29146  opphllem1  29156  opphllem2  29157  opphllem3  29158  opphllem4  29159  opphllem5  29160  opphllem6  29161  outpasch  29166  hlpasch  29167  lnopp2hpgb  29174  colhp  29181  lnincplng  29195  plngrotlem1  29198  plngrotlem2  29199  plngrot  29201  lnssplnglem  29202  lnssplng  29203  lmieu  29222  hypcgrlem1  29238  hypcgrlem2  29239  lnperpex  29242  trgcopy  29244  trgcopyeulem  29245  iscgra1  29250  cgrane2  29253  cgrane3  29254  cgrane4  29255  cgracgr  29258  cgraid  29259  cgraswap  29260  cgrcgra  29261  cgracom  29262  cgratr  29263  zerocgra  29264  flatcgra  29265  cgraswaplr  29266  cgracol  29269  dfcgra2  29271  sacgr  29272  oacgr  29273  acopy  29274  acopyeu  29275  ragcgra  29276  ragsupplcgra  29278  ragraghl  29279  perpeqlem  29280  perpeq  29281  tgaaddcpbllem1  29282  tgaaddcpbllem2  29283  tgaaddcpbllem3  29284  tgaaddcpbl  29285  tgaaddcpbl2  29286  leagne2  29302  leagne3  29303  cgrg3col4  29305  cgrabasimass  29311  angmgmaddeu1  29312  angmgmaddeu2  29313  angmgmaddeu3  29314  angmgmaddeu4  29315  angmgmaddeu5  29316  angmgmaddeu6  29317  angmgmaddeu7  29318  angmgmaddov1lem  29319  angmgmaddov2lem  29320  angmgmaddov1  29321  angmgmaddov2  29322  angmgmaddcpbl  29323  angmgmaddcl  29324  angmgmaddlid  29325  angmgmaddrid  29326  angmgmlem  29328  angmgm  29330  tgsas1  29332  tgsas2  29334  tgasa1  29336  dfprlng2  29358  dfprlng3  29359  perpprlng  29361  prlngex  29362  prlngmolem1  29363  prlngmolem2  29364  prlngmo2  29367  prlngmid2  29372  symquadprlng  29373  prlngsymquadlem  29374  prlngsymquadopp  29376  quadcgrprlng  29377  tgaltai  29378  ttgcontlem1  29395  brbtwn2  29416  axlowdimlem15  29467  axlowdimlem16  29468  axcontlem8  29482  upgrex  29603  edglnl  29654  umgrvad2edg  29727  nbupgr  29858  nbumgrvtx  29860  nbgr2vtx1edg  29864  nbuhgr2vtx1edgb  29866  nbupgrres  29878  cplgr3v  29949  cusgrexilem2  29956  usgredgsscusgredg  29973  1hegrvtxdg1r  30022  1egrvtxdg1r  30024  1egrvtxdg0  30025  pthdadjvtx  30246  pthdlem2lem  30286  wspniunwspnon  30445  umgr2cwwk2dif  30588  umgr2cycllem  30679  3pthdlem1  30698  uhgr3cyclex  30716  upgr4cycl4dv4e  30719  frgr3v  30809  1to3vfriswmgr  30814  frgrwopreglem5a  30845  frgrwopreglem3  30848  frgrhash2wsp  30866  staddi  32781  unidifsnne  33065  ifnefals  33077  coprprop  33225  sgnval2  33260  pmtrcnel  33583  pmtrcnel2  33584  psgnfzto1stlem  33594  cycpmco2lem1  33620  cycpmco2  33627  cyc2fvx  33628  cyc3co2  33634  cycpmrn  33637  tocyccntz  33638  cyc3evpm  33644  cyc3genpmlem  33645  isarchiofld  33693  drngidlhash  33916  mxidlnzr  33925  drng0mxidl  33933  drngmxidl  33934  qsdrng  33954  dflringlem3  33961  dflring3  33962  dflring4  33963  rsprprmprmidl  33987  deg1prod  34048  vietadeg1  34143  ply1annnr  34268  constrrtll  34296  constrrtlc1  34297  constrrtcclem  34299  constrrtcc  34300  constrfin  34311  constrelextdg2  34312  cos9thpiminplylem3  34349  1smat1  34369  submateqlem1  34372  ordtconnlem1  34489  esumrnmpt2  34633  cntnevol  34794  signstfveq0a  35139  repr0  35174  reprlt  35182  reprinfz1  35185  morleylemrneab  35234  nelscottrankgt  35679  cusgredgex  35827  2cycl2d  35833  acycgr1v  35835  derangenlem  35857  subfacp1lem1  35865  subfacp1lem3  35868  subfacp1lem5  35870  fmlasucdisj  36085  dfrdg4  36637  ifscgr  36731  cgrxfr  36742  btwnconn1lem8  36781  btwnconn3  36790  segcon2  36792  broutsideof3  36813  outsideoftr  36816  outsideofeq  36817  outsideofeu  36818  lineunray  36834  lineelsb2  36835  linethru  36840  mh-inf3sn  37252  unbdqndv2lem2  37298  knoppndvlem1  37300  knoppndvlem2  37301  knoppndvlem7  37306  knoppndvlem14  37313  bj-bary1lem  38151  bj-bary1lem1  38152  bj-bary1  38153  finxpreclem2  38233  finxp1o  38235  finxpreclem6  38239  fin2solem  38449  poimirlem9  38467  poimirlem15  38473  poimirlem20  38478  poimirlem24  38482  poimirlem25  38483  poimirlem27  38485  itg2addnclem2  38510  ftc1cnnc  38530  heibor1lem  38663  maxidln0  38899  lshpnelb  39961  lsatssn0  39979  lsatcv0  40008  lsat0cv  40010  lsatexch1  40023  l1cvat  40032  atlen0  40287  cvlsupr2  40320  atcvrj2b  40409  2atlt  40416  atbtwn  40423  3noncolr2  40426  4noncolr3  40430  3dimlem3  40438  3dimlem3OLDN  40439  3dimlem4  40441  3dimlem4OLDN  40442  3dim2  40445  1cvratex  40450  1cvrat  40453  ps-1  40454  ps-2  40455  hlatexch4  40458  3atlem4  40463  3atlem6  40465  4atlem0ae  40571  4atlem0be  40572  dalemccnedd  40664  dalemrotps  40668  dalem21  40671  dalem23  40673  dalem27  40676  dalem41  40690  dalem44  40693  dalem54  40703  lnatexN  40756  lnjatN  40757  llnexchb2lem  40845  llnexchb2  40846  lhpn0  40981  lhpexle3lem  40988  lhpmatb  41008  4atexlemswapqr  41040  4atexlemc  41046  4atexlemnclw  41047  4atexlemcnd  41049  4atexlemex4  41050  4atexlemex6  41051  4atex  41053  trlat  41146  trlval4  41165  cdlemc5  41172  cdlemd4  41178  cdlemd7  41181  cdlemd9  41183  cdleme0e  41194  cdleme3b  41206  cdleme3c  41207  cdleme3e  41209  cdleme3h  41212  cdleme7aa  41219  cdleme7e  41224  cdleme7ga  41225  cdleme9  41230  cdleme11c  41238  cdleme11e  41240  cdleme11fN  41241  cdleme11h  41243  cdleme11j  41244  cdleme11k  41245  cdleme15b  41252  cdleme15c  41253  cdleme17c  41265  cdleme18b  41269  cdlemesner  41273  cdleme20zN  41278  cdleme19c  41282  cdleme19d  41283  cdleme19e  41284  cdleme20m  41300  cdleme21a  41302  cdleme21b  41303  cdleme21c  41304  cdleme22f2  41324  cdleme28b  41348  cdleme36a  41437  cdleme36m  41438  cdleme41sn4aw  41452  cdleme43bN  41467  cdleme43dN  41469  cdleme46f2g2  41470  cdleme46f2g1  41471  cdleme4gfv  41484  cdlemeg46nlpq  41494  cdlemeg46req  41506  cdlemeg46fgN  41511  cdlemf1  41538  cdlemg8b  41605  cdlemg9a  41609  cdlemg12g  41626  cdlemg12  41627  cdlemg13a  41628  cdlemg17pq  41649  cdlemg18a  41655  cdlemg18c  41657  cdlemg19a  41660  cdlemg19  41661  cdlemg21  41663  cdlemg31b0N  41671  cdlemg31b0a  41672  cdlemg31c  41676  cdlemg33b0  41678  cdlemg33c0  41679  trlcone  41705  cdlemg42  41706  cdlemg44a  41708  cdlemg46  41712  cdlemh1  41792  cdlemh2  41793  cdlemh  41794  cdlemj3  41800  cdlemk3  41810  cdlemki  41818  cdlemksv2  41824  cdlemk12  41827  cdlemk14  41831  cdlemk15  41832  cdlemk7u  41847  cdlemk11u  41848  cdlemk12u  41849  cdlemk21N  41850  cdlemk20  41851  cdlemk22  41870  cdlemk26-3  41883  cdlemk27-3  41884  cdlemk28-3  41885  cdlemkfid3N  41902  cdlemk11ta  41906  cdlemk47  41926  cdlemk54  41935  dia2dimlem1  42041  dochsat  42360  dochshpncl  42361  lclkrlem2b  42485  lcfrlem21  42540  baerlem5amN  42693  baerlem5bmN  42694  baerlem5abmN  42695  mapdindp4  42700  mapdheq2  42706  mapdheq2biN  42707  mapdh6aN  42712  mapdh6dN  42716  mapdh6eN  42717  mapdh6hN  42720  mapdh7eN  42725  mapdh7dN  42727  mapdh7fN  42728  mapdh8ab  42754  mapdh8ad  42756  mapdh8e  42761  mapdh9a  42766  mapdh9aOLDN  42767  hdmap1l6a  42786  hdmap1l6d  42790  hdmap1l6e  42791  hdmap1l6h  42794  hdmap1eulem  42799  hdmap1eulemOLDN  42800  hdmapval0  42810  hdmapeveclem  42811  hdmapval3lemN  42814  hdmap10lem  42816  hdmap11lem1  42818  hdmaprnlem3N  42827  hdmaprnlem9N  42834  hdmaprnlem3eN  42835  fzne2d  42950  lcmineqlem11  43009  3lexlogpow5ineq1  43024  3lexlogpow5ineq2  43025  3lexlogpow5ineq4  43026  3lexlogpow5ineq3  43027  3lexlogpow2ineq1  43028  3lexlogpow2ineq2  43029  3lexlogpow5ineq5  43030  aks4d1lem1  43032  dvrelog2b  43036  dvrelogpow2b  43038  aks4d1p1p3  43039  aks4d1p1p2  43040  aks4d1p1p4  43041  aks4d1p1p6  43043  aks4d1p1p7  43044  aks4d1p1p5  43045  aks4d1p1  43046  aks4d1p2  43047  aks4d1p3  43048  aks4d1p5  43050  aks4d1p6  43051  aks4d1p7d1  43052  aks4d1p7  43053  aks4d1p8d3  43056  aks4d1p8  43057  aks4d1p9  43058  fldhmf1  43060  aks6d1c2p2  43089  hashscontpow  43092  aks6d1c3  43093  aks6d1c5lem2  43108  2np3bcnp1  43114  2ap1caineq  43115  sticksstones1  43116  sticksstones2  43117  sticksstones10  43125  sticksstones12a  43127  sticksstones12  43128  sticksstones22  43138  aks6d1c6lem4  43143  aks6d1c7lem2  43151  unitscyglem2  43166  unitscyglem4  43168  aks5lem8  43171  xppss12  43203  mhpind  43544  jm2.26lem3  43946  rpnnen3lem  43976  rpnnen3  43977  imo72b2lem2  45111  imo72b2  45116  mnuprdlem1  45200  bcc0  45268  chordthmALT  45859  fnchoice  45967  refsum2cnlem1  45975  xrleneltd  46257  xrltned  46291  infleinf  46305  reclt0  46324  icoiccdif  46458  ressiooinf  46491  limcresiooub  46574  limcleqr  46576  limclner  46583  climxrre  46682  icccncfext  46819  cncfiooiccre  46827  dvnxpaek  46874  stoweidlem43  46975  stirlinglem5  47010  stirlinglem7  47012  dirkercncflem1  47035  fourierdlem24  47063  fourierdlem32  47071  fourierdlem33  47072  fourierdlem34  47073  fourierdlem35  47074  fourierdlem46  47084  fourierdlem48  47086  fourierdlem49  47087  fourierdlem64  47102  fourierdlem65  47103  fourierdlem74  47112  fourierdlem76  47114  fourierdlem79  47117  fourierdlem81  47119  fourierdlem91  47129  fourierdlem102  47140  fourierdlem114  47152  etransclem15  47181  etransclem24  47190  sge0rpcpnf  47353  sge0isum  47359  pimrecltpos  47640  sqrtnnaa  47835  m1modne  48346  minusmod5ne  48347  m1modnep2mod  48350  modmknepk  48360  modm2nep1  48364  modm1nep2  48366  setsnidel  48381  odz2prm2pw  48570  fmtnoprmfac1lem  48571  fmtnoprmfac1  48572  fmtnoprmfac2  48574  lighneallem1  48612  lighneallem3  48614  perfectALTVlem2  48742  usgrgrtrirex  48970  isubgr3stgrlem6  48991  gpgusgralem  49076  gpg3nbgrvtx0  49096  pgnioedg1  49128  pgnioedg2  49129  pgnioedg5  49132  nnsgrpnmnd  49197  smprngprmrng  49358  lvecpsslmod  49541  affinecomb1  49736  affinecomb2  49737  1subrec1sub  49739  rrx2plord2  49756  line  49766  rrxline  49768  eenglngeehlnmlem2  49772  rrx2vlinest  49775  line2xlem  49787  2itscp  49815