Theorem necomd 2980

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

Syntax hints:   → wi 4   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  difsnb  4760  0nelop  5443  xpdifid  6121  f1ounsn  7213  resf1extb  7874  difsnen  8983  fofinf1o  9241  en2eleq  9921  en2other2  9922  ackbij1lem15  10146  infpssrlem5  10220  fin23lem24  10235  fin23lem31  10256  isf32lem9  10274  canthnumlem  10561  canthp1lem2  10566  npomex  10909  ltned  11270  lt0ne0  11604  recgt0  11988  zneo  12577  xrltne  13083  supxrbnd  13248  flltnz  13733  seqf1olem1  13966  nn0opthi  14195  hashtpg  14410  hash7g  14411  hashge3el3dif  14412  cats1un  14645  sumtp  15674  geoserg  15791  geolim  15795  geolim2  15796  tanadd  16094  ruclem6  16162  ruclem7  16163  isprm2lem  16610  isprm5  16636  oddprm  16740  pcmpt  16822  cshwshashlem3  17027  resshom  17340  ressco  17341  mrissmrcd  17564  rescco  17757  estrres  18063  smndex2dnrinv  18807  pmtrprfv  19350  symggen  19367  dprdcntz  19907  dprdres  19927  ablfac1b  19969  01eq0ringOLD  20434  nrhmzr  20440  ornglmullt  20772  orngrmullt  20773  orngmullt  20774  ofldlt1  20778  lbspss  21004  lspsnnecom  21044  lspindp2l  21059  lspindp2  21060  islbs3  21080  lbsextlem4  21086  lidlnz  21167  ofldchr  21501  uvcf1  21717  frlmup2  21724  psrridm  21888  coe1tmfv2  22177  coe1tmmul  22179  dmatmul  22400  mdetralt  22511  mdetunilem2  22516  mdetunilem6  22520  mdetunilem7  22521  maducoeval2  22543  madurid  22547  fvmptnn04ifa  22753  en2top  22888  cmpfi  23311  snfil  23767  tsmsfbas  24031  zcld  24718  iccpnfhmeo  24859  xrhmeo  24860  evth  24874  minveclem3b  25344  i1fres  25622  dvcnvlem  25896  ig1peu  26096  ig1pdvds  26101  aaliou3lem9  26274  taylthlem2  26298  taylthlem2OLD  26299  abelthlem2  26358  abelthlem7  26364  cos02pilt1  26451  tanregt0  26464  logcj  26531  argimgt0  26537  dvloglem  26573  logf1o2  26575  logbrec  26708  ang180lem1  26735  ang180lem2  26736  ang180lem3  26737  ang180lem4  26738  ang180lem5  26739  ang180  26740  isosctrlem3  26746  ssscongptld  26748  affineequivne  26753  angpieqvdlem  26754  angpieqvdlem2  26755  angpieqvd  26757  chordthmlem  26758  chordthmlem2  26759  chordthm  26763  asinneg  26812  ppiltx  27103  perfectlem2  27157  lgsneg  27248  lgsqr  27278  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem3  27309  lgsquad2  27313  2lgsoddprm  27343  dchrisum0flblem1  27435  noseponlem  27592  nosep1o  27609  nosep2o  27610  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem4  27664  noetainflem4  27668  slerec  27748  0elright  27844  tgbtwnouttr  28460  tgifscgr  28471  tgcgrxfr  28481  tglngval  28514  tgfscgr  28531  tgbtwnconn1lem3  28537  tgbtwnconn3  28540  legtrid  28554  hltr  28573  hlbtwn  28574  btwnhl1  28575  btwnhl  28577  hlcgrex  28579  hlcgreulem  28580  lncom  28585  tgisline  28590  tglineeltr  28594  tglineelsb2  28595  tglinecom  28598  tglinethru  28599  ncolncol  28609  coltr  28610  coltr3  28611  symquadlem  28652  midexlem  28655  ragcol  28662  ragcgr  28670  perpneq  28677  footexALT  28681  footexlem1  28682  footexlem2  28683  foot  28685  footne  28686  colperpexlem3  28695  mideulem2  28697  opphllem  28698  midex  28700  opphllem1  28710  opphllem2  28711  opphllem3  28712  opphllem4  28713  opphllem5  28714  opphllem6  28715  outpasch  28718  hlpasch  28719  lnopp2hpgb  28726  colhp  28733  lmieu  28747  hypcgrlem1  28762  hypcgrlem2  28763  lnperpex  28766  trgcopy  28767  trgcopyeulem  28768  iscgra1  28773  cgrane2  28776  cgrane3  28777  cgrane4  28778  cgracgr  28781  cgraid  28782  cgraswap  28783  cgrcgra  28784  cgracom  28785  cgratr  28786  flatcgra  28787  cgraswaplr  28788  cgracol  28791  dfcgra2  28793  sacgr  28794  oacgr  28795  acopy  28796  acopyeu  28797  leagne2  28813  leagne3  28814  cgrg3col4  28816  tgsas1  28817  tgsas2  28819  tgasa1  28821  ttgcontlem1  28848  brbtwn2  28868  axlowdimlem15  28919  axlowdimlem16  28920  axcontlem8  28934  upgrex  29055  edglnl  29106  umgrvad2edg  29176  nbupgr  29307  nbumgrvtx  29309  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  nbupgrres  29327  cplgr3v  29398  cusgrexilem2  29405  usgredgsscusgredg  29423  1hegrvtxdg1r  29472  1egrvtxdg1r  29474  1egrvtxdg0  29475  pthdadjvtx  29691  pthdlem2lem  29730  wspniunwspnon  29886  umgr2cwwk2dif  30026  3pthdlem1  30126  uhgr3cyclex  30144  upgr4cycl4dv4e  30147  frgr3v  30237  1to3vfriswmgr  30242  frgrwopreglem5a  30273  frgrwopreglem3  30276  frgrhash2wsp  30294  staddi  32208  unidifsnne  32498  ifnefals  32510  coprprop  32655  sgnval2  32691  pmtrcnel  33044  pmtrcnel2  33045  psgnfzto1stlem  33055  cycpmco2lem1  33081  cycpmco2  33088  cyc2fvx  33089  cyc3co2  33095  cycpmrn  33098  tocyccntz  33099  cyc3evpm  33105  cyc3genpmlem  33106  isarchiofld  33151  drngidlhash  33381  qsidomlem2  33400  ssdifidlprm  33405  mxidlnzr  33414  drng0mxidl  33423  drngmxidl  33424  qsdrng  33444  rsprprmprmidl  33469  ply1annnr  33669  constrrtll  33697  constrrtlc1  33698  constrrtcclem  33700  constrrtcc  33701  constrfin  33712  constrelextdg2  33713  cos9thpiminplylem3  33750  1smat1  33770  submateqlem1  33773  ordtconnlem1  33890  esumrnmpt2  34034  cntnevol  34194  signstfveq0a  34543  repr0  34578  reprlt  34586  reprinfz1  34589  cusgredgex  35094  2cycl2d  35111  acycgr1v  35121  derangenlem  35143  subfacp1lem1  35151  subfacp1lem3  35154  subfacp1lem5  35156  fmlasucdisj  35371  dfrdg4  35924  ifscgr  36017  cgrxfr  36028  btwnconn1lem8  36067  btwnconn3  36076  segcon2  36078  broutsideof3  36099  outsideoftr  36102  outsideofeq  36103  outsideofeu  36104  lineunray  36120  lineelsb2  36121  linethru  36126  unbdqndv2lem2  36483  knoppndvlem1  36485  knoppndvlem2  36486  knoppndvlem7  36491  knoppndvlem14  36498  bj-bary1lem  37283  bj-bary1lem1  37284  bj-bary1  37285  finxpreclem2  37363  finxp1o  37365  finxpreclem6  37369  fin2solem  37585  poimirlem9  37608  poimirlem15  37614  poimirlem20  37619  poimirlem24  37623  poimirlem25  37624  poimirlem27  37626  itg2addnclem2  37651  ftc1cnnc  37671  heibor1lem  37788  maxidln0  38024  lshpnelb  38962  lsatssn0  38980  lsatcv0  39009  lsat0cv  39011  lsatexch1  39024  l1cvat  39033  atlen0  39288  cvlsupr2  39321  atcvrj2b  39411  2atlt  39418  atbtwn  39425  3noncolr2  39428  4noncolr3  39432  3dimlem3  39440  3dimlem3OLDN  39441  3dimlem4  39443  3dimlem4OLDN  39444  3dim2  39447  1cvratex  39452  1cvrat  39455  ps-1  39456  ps-2  39457  hlatexch4  39460  3atlem4  39465  3atlem6  39467  4atlem0ae  39573  4atlem0be  39574  dalemccnedd  39666  dalemrotps  39670  dalem21  39673  dalem23  39675  dalem27  39678  dalem41  39692  dalem44  39695  dalem54  39705  lnatexN  39758  lnjatN  39759  llnexchb2lem  39847  llnexchb2  39848  lhpn0  39983  lhpexle3lem  39990  lhpmatb  40010  4atexlemswapqr  40042  4atexlemc  40048  4atexlemnclw  40049  4atexlemcnd  40051  4atexlemex4  40052  4atexlemex6  40053  4atex  40055  trlat  40148  trlval4  40167  cdlemc5  40174  cdlemd4  40180  cdlemd7  40183  cdlemd9  40185  cdleme0e  40196  cdleme3b  40208  cdleme3c  40209  cdleme3e  40211  cdleme3h  40214  cdleme7aa  40221  cdleme7e  40226  cdleme7ga  40227  cdleme9  40232  cdleme11c  40240  cdleme11e  40242  cdleme11fN  40243  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme15b  40254  cdleme15c  40255  cdleme17c  40267  cdleme18b  40271  cdlemesner  40275  cdleme20zN  40280  cdleme19c  40284  cdleme19d  40285  cdleme19e  40286  cdleme20m  40302  cdleme21a  40304  cdleme21b  40305  cdleme21c  40306  cdleme22f2  40326  cdleme28b  40350  cdleme36a  40439  cdleme36m  40440  cdleme41sn4aw  40454  cdleme43bN  40469  cdleme43dN  40471  cdleme46f2g2  40472  cdleme46f2g1  40473  cdleme4gfv  40486  cdlemeg46nlpq  40496  cdlemeg46req  40508  cdlemeg46fgN  40513  cdlemf1  40540  cdlemg8b  40607  cdlemg9a  40611  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg17pq  40651  cdlemg18a  40657  cdlemg18c  40659  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg31b0N  40673  cdlemg31b0a  40674  cdlemg31c  40678  cdlemg33b0  40680  cdlemg33c0  40681  trlcone  40707  cdlemg42  40708  cdlemg44a  40710  cdlemg46  40714  cdlemh1  40794  cdlemh2  40795  cdlemh  40796  cdlemj3  40802  cdlemk3  40812  cdlemki  40820  cdlemksv2  40826  cdlemk12  40829  cdlemk14  40833  cdlemk15  40834  cdlemk7u  40849  cdlemk11u  40850  cdlemk12u  40851  cdlemk21N  40852  cdlemk20  40853  cdlemk22  40872  cdlemk26-3  40885  cdlemk27-3  40886  cdlemk28-3  40887  cdlemkfid3N  40904  cdlemk11ta  40908  cdlemk47  40928  cdlemk54  40937  dia2dimlem1  41043  dochsat  41362  dochshpncl  41363  lclkrlem2b  41487  lcfrlem21  41542  baerlem5amN  41695  baerlem5bmN  41696  baerlem5abmN  41697  mapdindp4  41702  mapdheq2  41708  mapdheq2biN  41709  mapdh6aN  41714  mapdh6dN  41718  mapdh6eN  41719  mapdh6hN  41722  mapdh7eN  41727  mapdh7dN  41729  mapdh7fN  41730  mapdh8ab  41756  mapdh8ad  41758  mapdh8e  41763  mapdh9a  41768  mapdh9aOLDN  41769  hdmap1l6a  41788  hdmap1l6d  41792  hdmap1l6e  41793  hdmap1l6h  41796  hdmap1eulem  41801  hdmap1eulemOLDN  41802  hdmapval0  41812  hdmapeveclem  41813  hdmapval3lemN  41816  hdmap10lem  41818  hdmap11lem1  41820  hdmaprnlem3N  41829  hdmaprnlem9N  41836  hdmaprnlem3eN  41837  fzne2d  41953  lcmineqlem11  42012  3lexlogpow5ineq1  42027  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow5ineq3  42030  3lexlogpow2ineq1  42031  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1lem1  42035  dvrelog2b  42039  dvrelogpow2b  42041  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8d3  42059  aks4d1p8  42060  aks4d1p9  42061  fldhmf1  42063  aks6d1c2p2  42092  hashscontpow  42095  aks6d1c3  42096  aks6d1c5lem2  42111  2np3bcnp1  42117  2ap1caineq  42118  sticksstones1  42119  sticksstones2  42120  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  aks6d1c6lem4  42146  aks6d1c7lem2  42154  unitscyglem2  42169  unitscyglem4  42171  aks5lem8  42174  xppss12  42202  mhpind  42567  jm2.26lem3  42974  rpnnen3lem  43004  rpnnen3  43005  imo72b2lem2  44140  imo72b2  44145  mnuprdlem1  44245  bcc0  44313  chordthmALT  44906  fnchoice  45007  refsum2cnlem1  45015  xrleneltd  45303  xrltned  45337  infleinf  45352  reclt0  45371  icoiccdif  45506  ressiooinf  45539  limcresiooub  45624  limcleqr  45626  limclner  45633  climxrre  45732  icccncfext  45869  cncfiooiccre  45877  dvnxpaek  45924  stoweidlem43  46025  stirlinglem5  46060  stirlinglem7  46062  dirkercncflem1  46085  fourierdlem24  46113  fourierdlem32  46121  fourierdlem33  46122  fourierdlem34  46123  fourierdlem35  46124  fourierdlem46  46134  fourierdlem48  46136  fourierdlem49  46137  fourierdlem64  46152  fourierdlem65  46153  fourierdlem74  46162  fourierdlem76  46164  fourierdlem79  46167  fourierdlem81  46169  fourierdlem91  46179  fourierdlem102  46190  fourierdlem114  46202  etransclem15  46231  etransclem24  46240  sge0rpcpnf  46403  sge0isum  46409  pimrecltpos  46690  pimiooltgt  46692  m1modne  47333  minusmod5ne  47334  m1modnep2mod  47337  modmknepk  47347  modm2nep1  47351  modm1nep2  47353  setsnidel  47362  odz2prm2pw  47548  fmtnoprmfac1lem  47549  fmtnoprmfac1  47550  fmtnoprmfac2  47552  lighneallem1  47590  lighneallem3  47592  perfectALTVlem2  47707  usgrgrtrirex  47933  isubgr3stgrlem6  47954  gpgusgralem  48031  gpg3nbgrvtx0  48051  pgnioedg1  48082  pgnioedg2  48083  pgnioedg5  48086  nnsgrpnmnd  48150  lvecpsslmod  48480  affinecomb1  48675  affinecomb2  48676  1subrec1sub  48678  rrx2plord2  48695  line  48705  rrxline  48707  eenglngeehlnmlem2  48711  rrx2vlinest  48714  line2xlem  48726  2itscp  48754