Theorem necomd 2981

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 2979	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 218	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-ne 2927

This theorem is referenced by:  difsnb  4756  0nelop  5434  xpdifid  6112  f1ounsn  7201  resf1extb  7859  difsnen  8967  fofinf1o  9211  en2eleq  9891  en2other2  9892  ackbij1lem15  10116  infpssrlem5  10190  fin23lem24  10205  fin23lem31  10226  isf32lem9  10244  canthnumlem  10531  canthp1lem2  10536  npomex  10879  ltned  11241  lt0ne0  11575  recgt0  11959  zneo  12548  xrltne  13054  supxrbnd  13219  flltnz  13707  seqf1olem1  13940  nn0opthi  14169  hashtpg  14384  hash7g  14385  hashge3el3dif  14386  cats1un  14620  sumtp  15648  geoserg  15765  geolim  15769  geolim2  15770  tanadd  16068  ruclem6  16136  ruclem7  16137  isprm2lem  16584  isprm5  16610  oddprm  16714  pcmpt  16796  cshwshashlem3  17001  resshom  17314  ressco  17315  mrissmrcd  17538  rescco  17731  estrres  18037  chnccat  18524  chnrev  18525  chnpof1  18528  smndex2dnrinv  18815  pmtrprfv  19358  symggen  19375  dprdcntz  19915  dprdres  19935  ablfac1b  19977  01eq0ringOLD  20439  nrhmzr  20445  ornglmullt  20777  orngrmullt  20778  orngmullt  20779  ofldlt1  20783  lbspss  21009  lspsnnecom  21049  lspindp2l  21064  lspindp2  21065  islbs3  21085  lbsextlem4  21091  lidlnz  21172  ofldchr  21506  uvcf1  21722  frlmup2  21729  psrridm  21893  coe1tmfv2  22182  coe1tmmul  22184  dmatmul  22405  mdetralt  22516  mdetunilem2  22521  mdetunilem6  22525  mdetunilem7  22526  maducoeval2  22548  madurid  22552  fvmptnn04ifa  22758  en2top  22893  cmpfi  23316  snfil  23772  tsmsfbas  24036  zcld  24722  iccpnfhmeo  24863  xrhmeo  24864  evth  24878  minveclem3b  25348  i1fres  25626  dvcnvlem  25900  ig1peu  26100  ig1pdvds  26105  aaliou3lem9  26278  taylthlem2  26302  taylthlem2OLD  26303  abelthlem2  26362  abelthlem7  26368  cos02pilt1  26455  tanregt0  26468  logcj  26535  argimgt0  26541  dvloglem  26577  logf1o2  26579  logbrec  26712  ang180lem1  26739  ang180lem2  26740  ang180lem3  26741  ang180lem4  26742  ang180lem5  26743  ang180  26744  isosctrlem3  26750  ssscongptld  26752  affineequivne  26757  angpieqvdlem  26758  angpieqvdlem2  26759  angpieqvd  26761  chordthmlem  26762  chordthmlem2  26763  chordthm  26767  asinneg  26816  ppiltx  27107  perfectlem2  27161  lgsneg  27252  lgsqr  27282  lgseisenlem4  27309  lgsquadlem1  27311  lgsquadlem3  27313  lgsquad2  27317  2lgsoddprm  27347  dchrisum0flblem1  27439  noseponlem  27596  nosep1o  27613  nosep2o  27614  nosupbnd2lem1  27647  noinfbnd2lem1  27662  noetasuplem4  27668  noetainflem4  27672  slerec  27753  0elright  27850  tgbtwnouttr  28468  tgifscgr  28479  tgcgrxfr  28489  tglngval  28522  tgfscgr  28539  tgbtwnconn1lem3  28545  tgbtwnconn3  28548  legtrid  28562  hltr  28581  hlbtwn  28582  btwnhl1  28583  btwnhl  28585  hlcgrex  28587  hlcgreulem  28588  lncom  28593  tgisline  28598  tglineeltr  28602  tglineelsb2  28603  tglinecom  28606  tglinethru  28607  ncolncol  28617  coltr  28618  coltr3  28619  symquadlem  28660  midexlem  28663  ragcol  28670  ragcgr  28678  perpneq  28685  footexALT  28689  footexlem1  28690  footexlem2  28691  foot  28693  footne  28694  colperpexlem3  28703  mideulem2  28705  opphllem  28706  midex  28708  opphllem1  28718  opphllem2  28719  opphllem3  28720  opphllem4  28721  opphllem5  28722  opphllem6  28723  outpasch  28726  hlpasch  28727  lnopp2hpgb  28734  colhp  28741  lmieu  28755  hypcgrlem1  28770  hypcgrlem2  28771  lnperpex  28774  trgcopy  28775  trgcopyeulem  28776  iscgra1  28781  cgrane2  28784  cgrane3  28785  cgrane4  28786  cgracgr  28789  cgraid  28790  cgraswap  28791  cgrcgra  28792  cgracom  28793  cgratr  28794  flatcgra  28795  cgraswaplr  28796  cgracol  28799  dfcgra2  28801  sacgr  28802  oacgr  28803  acopy  28804  acopyeu  28805  leagne2  28821  leagne3  28822  cgrg3col4  28824  tgsas1  28825  tgsas2  28827  tgasa1  28829  ttgcontlem1  28856  brbtwn2  28876  axlowdimlem15  28927  axlowdimlem16  28928  axcontlem8  28942  upgrex  29063  edglnl  29114  umgrvad2edg  29184  nbupgr  29315  nbumgrvtx  29317  nbgr2vtx1edg  29321  nbuhgr2vtx1edgb  29323  nbupgrres  29335  cplgr3v  29406  cusgrexilem2  29413  usgredgsscusgredg  29431  1hegrvtxdg1r  29480  1egrvtxdg1r  29482  1egrvtxdg0  29483  pthdadjvtx  29699  pthdlem2lem  29738  wspniunwspnon  29894  umgr2cwwk2dif  30034  3pthdlem1  30134  uhgr3cyclex  30152  upgr4cycl4dv4e  30155  frgr3v  30245  1to3vfriswmgr  30250  frgrwopreglem5a  30281  frgrwopreglem3  30284  frgrhash2wsp  30302  staddi  32216  unidifsnne  32506  ifnefals  32518  coprprop  32670  sgnval2  32708  pmtrcnel  33048  pmtrcnel2  33049  psgnfzto1stlem  33059  cycpmco2lem1  33085  cycpmco2  33092  cyc2fvx  33093  cyc3co2  33099  cycpmrn  33102  tocyccntz  33103  cyc3evpm  33109  cyc3genpmlem  33110  isarchiofld  33158  drngidlhash  33389  qsidomlem2  33408  ssdifidlprm  33413  mxidlnzr  33422  drng0mxidl  33431  drngmxidl  33432  qsdrng  33452  rsprprmprmidl  33477  ply1annnr  33706  constrrtll  33734  constrrtlc1  33735  constrrtcclem  33737  constrrtcc  33738  constrfin  33749  constrelextdg2  33750  cos9thpiminplylem3  33787  1smat1  33807  submateqlem1  33810  ordtconnlem1  33927  esumrnmpt2  34071  cntnevol  34231  signstfveq0a  34579  repr0  34614  reprlt  34622  reprinfz1  34625  cusgredgex  35134  2cycl2d  35151  acycgr1v  35161  derangenlem  35183  subfacp1lem1  35191  subfacp1lem3  35194  subfacp1lem5  35196  fmlasucdisj  35411  dfrdg4  35964  ifscgr  36057  cgrxfr  36068  btwnconn1lem8  36107  btwnconn3  36116  segcon2  36118  broutsideof3  36139  outsideoftr  36142  outsideofeq  36143  outsideofeu  36144  lineunray  36160  lineelsb2  36161  linethru  36166  unbdqndv2lem2  36523  knoppndvlem1  36525  knoppndvlem2  36526  knoppndvlem7  36531  knoppndvlem14  36538  bj-bary1lem  37323  bj-bary1lem1  37324  bj-bary1  37325  finxpreclem2  37403  finxp1o  37405  finxpreclem6  37409  fin2solem  37625  poimirlem9  37648  poimirlem15  37654  poimirlem20  37659  poimirlem24  37663  poimirlem25  37664  poimirlem27  37666  itg2addnclem2  37691  ftc1cnnc  37711  heibor1lem  37828  maxidln0  38064  lshpnelb  39002  lsatssn0  39020  lsatcv0  39049  lsat0cv  39051  lsatexch1  39064  l1cvat  39073  atlen0  39328  cvlsupr2  39361  atcvrj2b  39450  2atlt  39457  atbtwn  39464  3noncolr2  39467  4noncolr3  39471  3dimlem3  39479  3dimlem3OLDN  39480  3dimlem4  39482  3dimlem4OLDN  39483  3dim2  39486  1cvratex  39491  1cvrat  39494  ps-1  39495  ps-2  39496  hlatexch4  39499  3atlem4  39504  3atlem6  39506  4atlem0ae  39612  4atlem0be  39613  dalemccnedd  39705  dalemrotps  39709  dalem21  39712  dalem23  39714  dalem27  39717  dalem41  39731  dalem44  39734  dalem54  39744  lnatexN  39797  lnjatN  39798  llnexchb2lem  39886  llnexchb2  39887  lhpn0  40022  lhpexle3lem  40029  lhpmatb  40049  4atexlemswapqr  40081  4atexlemc  40087  4atexlemnclw  40088  4atexlemcnd  40090  4atexlemex4  40091  4atexlemex6  40092  4atex  40094  trlat  40187  trlval4  40206  cdlemc5  40213  cdlemd4  40219  cdlemd7  40222  cdlemd9  40224  cdleme0e  40235  cdleme3b  40247  cdleme3c  40248  cdleme3e  40250  cdleme3h  40253  cdleme7aa  40260  cdleme7e  40265  cdleme7ga  40266  cdleme9  40271  cdleme11c  40279  cdleme11e  40281  cdleme11fN  40282  cdleme11h  40284  cdleme11j  40285  cdleme11k  40286  cdleme15b  40293  cdleme15c  40294  cdleme17c  40306  cdleme18b  40310  cdlemesner  40314  cdleme20zN  40319  cdleme19c  40323  cdleme19d  40324  cdleme19e  40325  cdleme20m  40341  cdleme21a  40343  cdleme21b  40344  cdleme21c  40345  cdleme22f2  40365  cdleme28b  40389  cdleme36a  40478  cdleme36m  40479  cdleme41sn4aw  40493  cdleme43bN  40508  cdleme43dN  40510  cdleme46f2g2  40511  cdleme46f2g1  40512  cdleme4gfv  40525  cdlemeg46nlpq  40535  cdlemeg46req  40547  cdlemeg46fgN  40552  cdlemf1  40579  cdlemg8b  40646  cdlemg9a  40650  cdlemg12g  40667  cdlemg12  40668  cdlemg13a  40669  cdlemg17pq  40690  cdlemg18a  40696  cdlemg18c  40698  cdlemg19a  40701  cdlemg19  40702  cdlemg21  40704  cdlemg31b0N  40712  cdlemg31b0a  40713  cdlemg31c  40717  cdlemg33b0  40719  cdlemg33c0  40720  trlcone  40746  cdlemg42  40747  cdlemg44a  40749  cdlemg46  40753  cdlemh1  40833  cdlemh2  40834  cdlemh  40835  cdlemj3  40841  cdlemk3  40851  cdlemki  40859  cdlemksv2  40865  cdlemk12  40868  cdlemk14  40872  cdlemk15  40873  cdlemk7u  40888  cdlemk11u  40889  cdlemk12u  40890  cdlemk21N  40891  cdlemk20  40892  cdlemk22  40911  cdlemk26-3  40924  cdlemk27-3  40925  cdlemk28-3  40926  cdlemkfid3N  40943  cdlemk11ta  40947  cdlemk47  40967  cdlemk54  40976  dia2dimlem1  41082  dochsat  41401  dochshpncl  41402  lclkrlem2b  41526  lcfrlem21  41581  baerlem5amN  41734  baerlem5bmN  41735  baerlem5abmN  41736  mapdindp4  41741  mapdheq2  41747  mapdheq2biN  41748  mapdh6aN  41753  mapdh6dN  41757  mapdh6eN  41758  mapdh6hN  41761  mapdh7eN  41766  mapdh7dN  41768  mapdh7fN  41769  mapdh8ab  41795  mapdh8ad  41797  mapdh8e  41802  mapdh9a  41807  mapdh9aOLDN  41808  hdmap1l6a  41827  hdmap1l6d  41831  hdmap1l6e  41832  hdmap1l6h  41835  hdmap1eulem  41840  hdmap1eulemOLDN  41841  hdmapval0  41851  hdmapeveclem  41852  hdmapval3lemN  41855  hdmap10lem  41857  hdmap11lem1  41859  hdmaprnlem3N  41868  hdmaprnlem9N  41875  hdmaprnlem3eN  41876  fzne2d  41992  lcmineqlem11  42051  3lexlogpow5ineq1  42066  3lexlogpow5ineq2  42067  3lexlogpow5ineq4  42068  3lexlogpow5ineq3  42069  3lexlogpow2ineq1  42070  3lexlogpow2ineq2  42071  3lexlogpow5ineq5  42072  aks4d1lem1  42074  dvrelog2b  42078  dvrelogpow2b  42080  aks4d1p1p3  42081  aks4d1p1p2  42082  aks4d1p1p4  42083  aks4d1p1p6  42085  aks4d1p1p7  42086  aks4d1p1p5  42087  aks4d1p1  42088  aks4d1p2  42089  aks4d1p3  42090  aks4d1p5  42092  aks4d1p6  42093  aks4d1p7d1  42094  aks4d1p7  42095  aks4d1p8d3  42098  aks4d1p8  42099  aks4d1p9  42100  fldhmf1  42102  aks6d1c2p2  42131  hashscontpow  42134  aks6d1c3  42135  aks6d1c5lem2  42150  2np3bcnp1  42156  2ap1caineq  42157  sticksstones1  42158  sticksstones2  42159  sticksstones10  42167  sticksstones12a  42169  sticksstones12  42170  sticksstones22  42180  aks6d1c6lem4  42185  aks6d1c7lem2  42193  unitscyglem2  42208  unitscyglem4  42210  aks5lem8  42213  xppss12  42241  mhpind  42606  jm2.26lem3  43013  rpnnen3lem  43043  rpnnen3  43044  imo72b2lem2  44179  imo72b2  44184  mnuprdlem1  44284  bcc0  44352  chordthmALT  44944  fnchoice  45045  refsum2cnlem1  45053  xrleneltd  45341  xrltned  45375  infleinf  45389  reclt0  45408  icoiccdif  45543  ressiooinf  45576  limcresiooub  45659  limcleqr  45661  limclner  45668  climxrre  45767  icccncfext  45904  cncfiooiccre  45912  dvnxpaek  45959  stoweidlem43  46060  stirlinglem5  46095  stirlinglem7  46097  dirkercncflem1  46120  fourierdlem24  46148  fourierdlem32  46156  fourierdlem33  46157  fourierdlem34  46158  fourierdlem35  46159  fourierdlem46  46169  fourierdlem48  46171  fourierdlem49  46172  fourierdlem64  46187  fourierdlem65  46188  fourierdlem74  46197  fourierdlem76  46199  fourierdlem79  46202  fourierdlem81  46204  fourierdlem91  46214  fourierdlem102  46225  fourierdlem114  46237  etransclem15  46266  etransclem24  46275  sge0rpcpnf  46438  sge0isum  46444  pimrecltpos  46725  pimiooltgt  46727  m1modne  47358  minusmod5ne  47359  m1modnep2mod  47362  modmknepk  47372  modm2nep1  47376  modm1nep2  47378  setsnidel  47387  odz2prm2pw  47573  fmtnoprmfac1lem  47574  fmtnoprmfac1  47575  fmtnoprmfac2  47577  lighneallem1  47615  lighneallem3  47617  perfectALTVlem2  47732  usgrgrtrirex  47960  isubgr3stgrlem6  47981  gpgusgralem  48066  gpg3nbgrvtx0  48086  pgnioedg1  48118  pgnioedg2  48119  pgnioedg5  48122  nnsgrpnmnd  48188  lvecpsslmod  48518  affinecomb1  48713  affinecomb2  48714  1subrec1sub  48716  rrx2plord2  48733  line  48743  rrxline  48745  eenglngeehlnmlem2  48749  rrx2vlinest  48752  line2xlem  48764  2itscp  48792