Theorem necomd 3002

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

Syntax hints:   → wi 4   ≠ wne 2947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-ne 2948

This theorem is referenced by:  difsnb  4756  0nelop  5455  xpdifid  6139  f1ounsn  7241  resf1extb  7900  difsnen  9016  fofinf1o  9261  en2eleq  9950  en2other2  9951  ackbij1lem15  10175  infpssrlem5  10250  fin23lem24  10265  fin23lem31  10286  isf32lem9  10304  canthnumlem  10592  canthp1lem2  10597  npomex  10940  ltned  11305  lt0ne0  11639  recgt0  12023  zneo  12642  xrltne  13151  supxrbnd  13317  flltnz  13807  seqf1olem1  14040  nn0opthi  14269  hashtpg  14484  hash7g  14485  hashge3el3dif  14486  cats1un  14720  sumtp  15748  geoserg  15868  geolim  15872  geolim2  15873  tanadd  16171  ruclem6  16239  ruclem7  16240  isprm2lem  16687  isprm5  16714  oddprm  16818  pcmpt  16900  cshwshashlem3  17105  resshom  17419  ressco  17420  mrissmrcd  17644  rescco  17837  estrres  18143  chnccat  18630  chnrev  18631  chnpof1  18634  smndex2dnrinv  18924  pmtrprfv  19465  symggen  19482  dprdcntz  20022  dprdres  20042  ablfac1b  20084  01eq0ringOLD  20549  nrhmzr  20555  ornglmullt  20887  orngrmullt  20888  orngmullt  20889  ofldlt1  20893  lbspss  21118  lspsnnecom  21158  lspindp2l  21173  lspindp2  21174  islbs3  21194  lbsextlem4  21200  lidlnz  21281  ofldchr  21597  uvcf1  21813  frlmup2  21820  psrridm  21983  coe1tmfv2  22307  coe1tmmul  22309  dmatmul  22526  mdetralt  22637  mdetunilem2  22642  mdetunilem6  22646  mdetunilem7  22647  maducoeval2  22669  madurid  22673  fvmptnn04ifa  22879  en2top  23014  cmpfi  23437  snfil  23893  tsmsfbas  24157  zcld  24843  iccpnfhmeo  24976  xrhmeo  24977  evth  24990  minveclem3b  25459  i1fres  25736  dvcnvlem  26007  ig1peu  26204  ig1pdvds  26209  aaliou3lem9  26380  taylthlem2  26403  abelthlem2  26461  abelthlem7  26467  cos02pilt1  26557  tanregt0  26570  logcj  26637  argimgt0  26643  dvloglem  26679  logf1o2  26681  logbrec  26813  ang180lem1  26840  ang180lem2  26841  ang180lem3  26842  ang180lem4  26843  ang180lem5  26844  ang180  26845  isosctrlem3  26851  ssscongptld  26853  affineequivne  26858  angpieqvdlem  26859  angpieqvdlem2  26860  angpieqvd  26862  chordthmlem  26863  chordthmlem2  26864  chordthm  26868  asinneg  26917  ppiltx  27207  perfectlem2  27260  lgsneg  27351  lgsqr  27381  lgseisenlem4  27408  lgsquadlem1  27410  lgsquadlem3  27412  lgsquad2  27416  2lgsoddprm  27446  dchrisum0flblem1  27538  noseponlem  27694  nosep1o  27711  nosep2o  27712  nosupbnd2lem1  27745  noinfbnd2lem1  27760  noetasuplem4  27766  noetainflem4  27770  lesrec  27858  0elright  27971  tgbtwnouttr  28632  tgifscgr  28643  tgcgrxfr  28653  tglngval  28686  tgfscgr  28703  tgbtwnconn1lem3  28709  tgbtwnconn3  28712  legtrid  28726  hltr  28745  hlbtwn  28746  btwnhl1  28747  btwnhl  28749  hlcgrex  28751  hlcgreulem  28752  lncom  28757  tgisline  28762  tglineeltr  28766  tglineelsb2  28767  tglinecom  28770  tglinethru  28771  ncolncol  28781  coltr  28782  coltr3  28783  symquadlem  28824  midexlem  28827  ragcol  28834  ragcgr  28842  perpneq  28849  footexALT  28853  footexlem1  28854  footexlem2  28855  foot  28857  footne  28858  colperpexlem3  28867  mideulem2  28869  opphllem  28870  midex  28872  opphllem1  28882  opphllem2  28883  opphllem3  28884  opphllem4  28885  opphllem5  28886  opphllem6  28887  outpasch  28890  hlpasch  28891  lnopp2hpgb  28898  colhp  28905  lmieu  28919  hypcgrlem1  28934  hypcgrlem2  28935  lnperpex  28938  trgcopy  28939  trgcopyeulem  28940  iscgra1  28945  cgrane2  28948  cgrane3  28949  cgrane4  28950  cgracgr  28953  cgraid  28954  cgraswap  28955  cgrcgra  28956  cgracom  28957  cgratr  28958  flatcgra  28959  cgraswaplr  28960  cgracol  28963  dfcgra2  28965  sacgr  28966  oacgr  28967  acopy  28968  acopyeu  28969  leagne2  28985  leagne3  28986  cgrg3col4  28988  tgsas1  28989  tgsas2  28991  tgasa1  28993  ttgcontlem1  29020  brbtwn2  29041  axlowdimlem15  29092  axlowdimlem16  29093  axcontlem8  29107  upgrex  29228  edglnl  29279  umgrvad2edg  29349  nbupgr  29480  nbumgrvtx  29482  nbgr2vtx1edg  29486  nbuhgr2vtx1edgb  29488  nbupgrres  29500  cplgr3v  29571  cusgrexilem2  29578  usgredgsscusgredg  29595  1hegrvtxdg1r  29644  1egrvtxdg1r  29646  1egrvtxdg0  29647  pthdadjvtx  29863  pthdlem2lem  29902  wspniunwspnon  30058  umgr2cwwk2dif  30201  3pthdlem1  30301  uhgr3cyclex  30319  upgr4cycl4dv4e  30322  frgr3v  30412  1to3vfriswmgr  30417  frgrwopreglem5a  30448  frgrwopreglem3  30451  frgrhash2wsp  30469  staddi  32384  unidifsnne  32673  ifnefals  32685  coprprop  32840  sgnval2  32876  pmtrcnel  33219  pmtrcnel2  33220  psgnfzto1stlem  33230  cycpmco2lem1  33256  cycpmco2  33263  cyc2fvx  33264  cyc3co2  33270  cycpmrn  33273  tocyccntz  33274  cyc3evpm  33280  cyc3genpmlem  33281  isarchiofld  33329  drngidlhash  33566  qsidomlem2  33585  ssdifidlprm  33590  mxidlnzr  33599  drng0mxidl  33608  drngmxidl  33609  qsdrng  33629  dflringlem3  33636  dflring3  33637  dflring4  33638  rsprprmprmidl  33662  deg1prod  33723  vietadeg1  33819  ply1annnr  33944  constrrtll  33972  constrrtlc1  33973  constrrtcclem  33975  constrrtcc  33976  constrfin  33987  constrelextdg2  33988  cos9thpiminplylem3  34025  1smat1  34045  submateqlem1  34048  ordtconnlem1  34165  esumrnmpt2  34309  cntnevol  34469  signstfveq0a  34817  repr0  34852  reprlt  34860  reprinfz1  34863  morleylemrneab  34912  cusgredgex  35410  2cycl2d  35427  acycgr1v  35437  derangenlem  35459  subfacp1lem1  35467  subfacp1lem3  35470  subfacp1lem5  35472  fmlasucdisj  35687  dfrdg4  36239  ifscgr  36332  cgrxfr  36343  btwnconn1lem8  36382  btwnconn3  36391  segcon2  36393  broutsideof3  36414  outsideoftr  36417  outsideofeq  36418  outsideofeu  36419  lineunray  36435  lineelsb2  36436  linethru  36441  mh-inf3f1  36839  mh-inf3sn  36840  unbdqndv2lem2  36886  knoppndvlem1  36888  knoppndvlem2  36889  knoppndvlem7  36894  knoppndvlem14  36901  bj-bary1lem  37740  bj-bary1lem1  37741  bj-bary1  37742  finxpreclem2  37822  finxp1o  37824  finxpreclem6  37828  fin2solem  38043  poimirlem9  38066  poimirlem15  38072  poimirlem20  38077  poimirlem24  38081  poimirlem25  38082  poimirlem27  38084  itg2addnclem2  38109  ftc1cnnc  38129  heibor1lem  38246  maxidln0  38482  lshpnelb  39546  lsatssn0  39564  lsatcv0  39593  lsat0cv  39595  lsatexch1  39608  l1cvat  39617  atlen0  39872  cvlsupr2  39905  atcvrj2b  39994  2atlt  40001  atbtwn  40008  3noncolr2  40011  4noncolr3  40015  3dimlem3  40023  3dimlem3OLDN  40024  3dimlem4  40026  3dimlem4OLDN  40027  3dim2  40030  1cvratex  40035  1cvrat  40038  ps-1  40039  ps-2  40040  hlatexch4  40043  3atlem4  40048  3atlem6  40050  4atlem0ae  40156  4atlem0be  40157  dalemccnedd  40249  dalemrotps  40253  dalem21  40256  dalem23  40258  dalem27  40261  dalem41  40275  dalem44  40278  dalem54  40288  lnatexN  40341  lnjatN  40342  llnexchb2lem  40430  llnexchb2  40431  lhpn0  40566  lhpexle3lem  40573  lhpmatb  40593  4atexlemswapqr  40625  4atexlemc  40631  4atexlemnclw  40632  4atexlemcnd  40634  4atexlemex4  40635  4atexlemex6  40636  4atex  40638  trlat  40731  trlval4  40750  cdlemc5  40757  cdlemd4  40763  cdlemd7  40766  cdlemd9  40768  cdleme0e  40779  cdleme3b  40791  cdleme3c  40792  cdleme3e  40794  cdleme3h  40797  cdleme7aa  40804  cdleme7e  40809  cdleme7ga  40810  cdleme9  40815  cdleme11c  40823  cdleme11e  40825  cdleme11fN  40826  cdleme11h  40828  cdleme11j  40829  cdleme11k  40830  cdleme15b  40837  cdleme15c  40838  cdleme17c  40850  cdleme18b  40854  cdlemesner  40858  cdleme20zN  40863  cdleme19c  40867  cdleme19d  40868  cdleme19e  40869  cdleme20m  40885  cdleme21a  40887  cdleme21b  40888  cdleme21c  40889  cdleme22f2  40909  cdleme28b  40933  cdleme36a  41022  cdleme36m  41023  cdleme41sn4aw  41037  cdleme43bN  41052  cdleme43dN  41054  cdleme46f2g2  41055  cdleme46f2g1  41056  cdleme4gfv  41069  cdlemeg46nlpq  41079  cdlemeg46req  41091  cdlemeg46fgN  41096  cdlemf1  41123  cdlemg8b  41190  cdlemg9a  41194  cdlemg12g  41211  cdlemg12  41212  cdlemg13a  41213  cdlemg17pq  41234  cdlemg18a  41240  cdlemg18c  41242  cdlemg19a  41245  cdlemg19  41246  cdlemg21  41248  cdlemg31b0N  41256  cdlemg31b0a  41257  cdlemg31c  41261  cdlemg33b0  41263  cdlemg33c0  41264  trlcone  41290  cdlemg42  41291  cdlemg44a  41293  cdlemg46  41297  cdlemh1  41377  cdlemh2  41378  cdlemh  41379  cdlemj3  41385  cdlemk3  41395  cdlemki  41403  cdlemksv2  41409  cdlemk12  41412  cdlemk14  41416  cdlemk15  41417  cdlemk7u  41432  cdlemk11u  41433  cdlemk12u  41434  cdlemk21N  41435  cdlemk20  41436  cdlemk22  41455  cdlemk26-3  41468  cdlemk27-3  41469  cdlemk28-3  41470  cdlemkfid3N  41487  cdlemk11ta  41491  cdlemk47  41511  cdlemk54  41520  dia2dimlem1  41626  dochsat  41945  dochshpncl  41946  lclkrlem2b  42070  lcfrlem21  42125  baerlem5amN  42278  baerlem5bmN  42279  baerlem5abmN  42280  mapdindp4  42285  mapdheq2  42291  mapdheq2biN  42292  mapdh6aN  42297  mapdh6dN  42301  mapdh6eN  42302  mapdh6hN  42305  mapdh7eN  42310  mapdh7dN  42312  mapdh7fN  42313  mapdh8ab  42339  mapdh8ad  42341  mapdh8e  42346  mapdh9a  42351  mapdh9aOLDN  42352  hdmap1l6a  42371  hdmap1l6d  42375  hdmap1l6e  42376  hdmap1l6h  42379  hdmap1eulem  42384  hdmap1eulemOLDN  42385  hdmapval0  42395  hdmapeveclem  42396  hdmapval3lemN  42399  hdmap10lem  42401  hdmap11lem1  42403  hdmaprnlem3N  42412  hdmaprnlem9N  42419  hdmaprnlem3eN  42420  fzne2d  42535  lcmineqlem11  42594  3lexlogpow5ineq1  42609  3lexlogpow5ineq2  42610  3lexlogpow5ineq4  42611  3lexlogpow5ineq3  42612  3lexlogpow2ineq1  42613  3lexlogpow2ineq2  42614  3lexlogpow5ineq5  42615  aks4d1lem1  42617  dvrelog2b  42621  dvrelogpow2b  42623  aks4d1p1p3  42624  aks4d1p1p2  42625  aks4d1p1p4  42626  aks4d1p1p6  42628  aks4d1p1p7  42629  aks4d1p1p5  42630  aks4d1p1  42631  aks4d1p2  42632  aks4d1p3  42633  aks4d1p5  42635  aks4d1p6  42636  aks4d1p7d1  42637  aks4d1p7  42638  aks4d1p8d3  42641  aks4d1p8  42642  aks4d1p9  42643  fldhmf1  42645  aks6d1c2p2  42674  hashscontpow  42677  aks6d1c3  42678  aks6d1c5lem2  42693  2np3bcnp1  42699  2ap1caineq  42700  sticksstones1  42701  sticksstones2  42702  sticksstones10  42710  sticksstones12a  42712  sticksstones12  42713  sticksstones22  42723  aks6d1c6lem4  42728  aks6d1c7lem2  42736  unitscyglem2  42751  unitscyglem4  42753  aks5lem8  42756  xppss12  42786  mhpind  43114  jm2.26lem3  43516  rpnnen3lem  43546  rpnnen3  43547  imo72b2lem2  44681  imo72b2  44686  mnuprdlem1  44786  bcc0  44854  chordthmALT  45446  fnchoice  45547  refsum2cnlem1  45555  xrleneltd  45837  xrltned  45871  infleinf  45885  reclt0  45904  icoiccdif  46038  ressiooinf  46071  limcresiooub  46154  limcleqr  46156  limclner  46163  climxrre  46262  icccncfext  46399  cncfiooiccre  46407  dvnxpaek  46454  stoweidlem43  46555  stirlinglem5  46590  stirlinglem7  46592  dirkercncflem1  46615  fourierdlem24  46643  fourierdlem32  46651  fourierdlem33  46652  fourierdlem34  46653  fourierdlem35  46654  fourierdlem46  46664  fourierdlem48  46666  fourierdlem49  46667  fourierdlem64  46682  fourierdlem65  46683  fourierdlem74  46692  fourierdlem76  46694  fourierdlem79  46697  fourierdlem81  46699  fourierdlem91  46709  fourierdlem102  46720  fourierdlem114  46732  etransclem15  46761  etransclem24  46770  sge0rpcpnf  46933  sge0isum  46939  pimrecltpos  47220  m1modne  47886  minusmod5ne  47887  m1modnep2mod  47890  modmknepk  47900  modm2nep1  47904  modm1nep2  47906  setsnidel  47921  odz2prm2pw  48110  fmtnoprmfac1lem  48111  fmtnoprmfac1  48112  fmtnoprmfac2  48114  lighneallem1  48152  lighneallem3  48154  perfectALTVlem2  48282  usgrgrtrirex  48510  isubgr3stgrlem6  48531  gpgusgralem  48616  gpg3nbgrvtx0  48636  pgnioedg1  48668  pgnioedg2  48669  pgnioedg5  48672  nnsgrpnmnd  48738  lvecpsslmod  49067  affinecomb1  49262  affinecomb2  49263  1subrec1sub  49265  rrx2plord2  49282  line  49292  rrxline  49294  eenglngeehlnmlem2  49298  rrx2vlinest  49301  line2xlem  49313  2itscp  49341