Theorem necomd 3014

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  difsnb  4769  0nelop  5472  xpdifid  6171  f1ounsn  7303  resf1extb  7970  difsnen  9106  fofinf1o  9349  en2eleq  10114  en2other2  10115  ackbij1lem15  10338  infpssrlem5  10412  fin23lem24  10427  fin23lem31  10448  isf32lem9  10466  canthnumlem  10760  canthp1lem2  10765  npomex  11108  ltned  11473  lt0ne0  11809  recgt0  12190  zneo  12809  xrltne  13319  supxrbnd  13485  flltnz  13978  seqf1olem1  14211  nn0opthi  14441  hashtpg  14657  hash7g  14658  hashge3el3dif  14659  cats1un  14898  sumtp  15944  geoserg  16064  geolim  16068  geolim2  16069  tanadd  16364  ruclem6  16432  ruclem7  16433  isprm2lem  16885  isprm5  16912  oddprm  17017  pcmpt  17099  cshwshashlem3  17304  resshom  17618  ressco  17619  mrissmrcd  17843  rescco  18036  estrres  18342  chnccat  18829  chnrev  18830  chnpof1  18833  smndex2dnrinv  19143  pmtrprfv  19697  symggen  19714  dprdcntz  20254  dprdres  20274  ablfac1b  20316  01eq0ringOLD  20812  nrhmzr  20819  zrdrng  21056  ornglmullt  21156  orngrmullt  21157  orngmullt  21158  ofldlt1  21162  lbspss  21387  lspsnnecom  21427  lspindp2l  21442  lspindp2  21443  islbs3  21463  lbsextlem4  21469  lidlnz  21560  isfieldidl  21570  qsidomlem2  21667  ssdifidlprm  21672  ofldchr  21912  uvcf1  22128  frlmup2  22135  psrridm  22300  coe1tmfv2  22624  coe1tmmul  22626  dmatmul  22842  mdetralt  22953  mdetunilem2  22958  mdetunilem6  22962  mdetunilem7  22963  maducoeval2  22985  madurid  22989  fvmptnn04ifa  23198  en2top  23333  cmpfi  23756  snfil  24213  tsmsfbas  24477  zcld  25163  iccpnfhmeo  25296  xrhmeo  25297  evth  25310  minveclem3b  25779  i1fres  26056  dvcnvlem  26326  ig1peu  26523  ig1pdvds  26528  aaliou3lem9  26707  taylthlem2  26731  abelthlem2  26789  abelthlem7  26795  cos02pilt1  26884  tanregt0  26897  logcj  26964  argimgt0  26970  dvloglem  27006  logf1o2  27008  logbrec  27140  ang180lem1  27167  ang180lem2  27168  ang180lem3  27169  ang180lem4  27170  ang180lem5  27171  ang180  27172  isosctrlem3  27178  ssscongptld  27180  affineequivne  27185  angpieqvdlem  27186  angpieqvdlem2  27187  angpieqvd  27189  chordthmlem  27190  chordthmlem2  27191  chordthm  27195  asinneg  27244  ppiltx  27534  perfectlem2  27587  lgsneg  27678  lgsqr  27708  lgseisenlem4  27735  lgsquadlem1  27737  lgsquadlem3  27739  lgsquad2  27743  2lgsoddprm  27773  dchrisum0flblem1  27865  noseponlem  28051  nosep1o  28068  nosep2o  28069  nosupbnd2lem1  28102  noinfbnd2lem1  28117  noetasuplem4  28123  noetainflem4  28127  lesrec  28215  0elright  28328  tgbtwnouttr  28990  tgifscgr  29001  tgcgrxfr  29011  tglngval  29044  tgfscgr  29061  tgbtwnconn1lem3  29067  tgbtwnconn3  29070  legtrid  29084  hltr  29106  hlbtwn  29107  btwnhl1  29108  btwnhl  29110  hlcgrex  29112  hlcgreulem  29113  lncom  29120  tgisline  29125  tglineeltr  29129  tglineelsb2  29130  tglinecom  29133  tglinethru  29134  ncolncol  29145  coltr  29146  coltr3  29147  tglnpt3  29152  tglnpt4  29153  symquadlem  29191  midexlem  29194  mirlni  29197  ragcol  29204  ragcgr  29212  perpneq  29219  footexALT  29223  footexlem1  29224  footexlem2  29225  foot  29227  footne  29228  colperpexlem3  29238  mideulem2  29240  opphllem  29241  midex  29243  opphllem1  29253  opphllem2  29254  opphllem3  29255  opphllem4  29256  opphllem5  29257  opphllem6  29258  outpasch  29263  hlpasch  29264  lnopp2hpgb  29271  colhp  29278  lnincplng  29292  plngrotlem1  29295  plngrotlem2  29296  plngrot  29298  lnssplnglem  29299  lnssplng  29300  lmieu  29319  hypcgrlem1  29335  hypcgrlem2  29336  lnperpex  29339  trgcopy  29341  trgcopyeulem  29342  iscgra1  29347  cgrane2  29350  cgrane3  29351  cgrane4  29352  cgracgr  29355  cgraid  29356  cgraswap  29357  cgrcgra  29358  cgracom  29359  cgratr  29360  zerocgra  29361  flatcgra  29362  cgraswaplr  29363  cgracol  29366  dfcgra2  29368  sacgr  29369  oacgr  29370  acopy  29371  acopyeu  29372  ragcgra  29373  ragsupplcgra  29375  ragraghl  29376  perpeqlem  29377  perpeq  29378  tgaaddcpbllem1  29379  tgaaddcpbllem2  29380  tgaaddcpbllem3  29381  tgaaddcpbl  29382  tgaaddcpbl2  29383  leagne2  29399  leagne3  29400  cgrg3col4  29402  cgrabasimass  29408  angmgmaddeu1  29409  angmgmaddeu2  29410  angmgmaddeu3  29411  angmgmaddeu4  29412  angmgmaddeu5  29413  angmgmaddeu6  29414  angmgmaddeu7  29415  angmgmaddov1lem  29416  angmgmaddov2lem  29417  angmgmaddov1  29418  angmgmaddov2  29419  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddlid  29422  angmgmaddrid  29423  angmgmlem  29425  angmgm  29427  tgsas1  29429  tgsas2  29431  tgasa1  29433  dfprlng2  29455  dfprlng3  29456  perpprlng  29458  prlngex  29459  prlngmolem1  29460  prlngmolem2  29461  prlngmo2  29464  prlngmid2  29469  symquadprlng  29470  prlngsymquadlem  29471  prlngsymquadopp  29473  quadcgrprlng  29474  tgaltai  29475  ttgcontlem1  29492  brbtwn2  29513  axlowdimlem15  29564  axlowdimlem16  29565  axcontlem8  29579  upgrex  29700  edglnl  29751  umgrvad2edg  29824  nbupgr  29955  nbumgrvtx  29957  nbgr2vtx1edg  29961  nbuhgr2vtx1edgb  29963  nbupgrres  29975  cplgr3v  30046  cusgrexilem2  30053  usgredgsscusgredg  30070  1hegrvtxdg1r  30119  1egrvtxdg1r  30121  1egrvtxdg0  30122  pthdadjvtx  30343  pthdlem2lem  30383  wspniunwspnon  30542  umgr2cwwk2dif  30685  umgr2cycllem  30776  3pthdlem1  30795  uhgr3cyclex  30813  upgr4cycl4dv4e  30816  frgr3v  30906  1to3vfriswmgr  30911  frgrwopreglem5a  30942  frgrwopreglem3  30945  frgrhash2wsp  30963  staddi  32878  cgrahlb  33077  inagbtwn  33078  inagcgrasubhl  33079  inagcgrasubbtwn  33080  inagcgrabtwn  33081  inagcgratrgmain  33084  inaglea  33089  tgmircgra  33096  tgextancd  33098  tgextahpl  33099  tgextalem1inag  33100  tgextamirnhl  33102  tgextancgra  33104  tgextalt1  33106  tgextalt2  33107  tgexta  33108  tgaasncol  33110  tgaasexc  33111  tgaasne  33112  tgaascgra  33113  tgaas1  33115  unidifsnne  33204  ifnefals  33216  coprprop  33363  sgnval2  33397  pmtrcnel  33720  pmtrcnel2  33721  psgnfzto1stlem  33731  cycpmco2lem1  33757  cycpmco2  33764  cyc2fvx  33765  cyc3co2  33771  cycpmrn  33774  tocyccntz  33775  cyc3evpm  33781  cyc3genpmlem  33782  isarchiofld  33830  drngidlhash  34053  mxidlnzr  34062  drng0mxidl  34070  drngmxidl  34071  qsdrng  34091  dflringlem3  34098  dflring3  34099  dflring4  34100  rsprprmprmidl  34124  deg1prod  34185  vietadeg1  34280  ply1annnr  34405  constrrtll  34433  constrrtlc1  34434  constrrtcclem  34436  constrrtcc  34437  constrfin  34448  constrelextdg2  34449  cos9thpiminplylem3  34486  1smat1  34506  submateqlem1  34509  ordtconnlem1  34626  esumrnmpt2  34770  cntnevol  34931  signstfveq0a  35275  repr0  35310  reprlt  35318  reprinfz1  35321  morleylemrneab  35370  nelscottrankgt  35833  cusgredgex  36063  2cycl2d  36069  acycgr1v  36071  derangenlem  36103  subfacp1lem1  36111  subfacp1lem3  36114  subfacp1lem5  36116  fmlasucdisj  36331  elpssex  36635  dfrdg4  36893  ifscgr  36987  cgrxfr  36998  btwnconn1lem8  37037  btwnconn3  37046  segcon2  37048  broutsideof3  37069  outsideoftr  37072  outsideofeq  37073  outsideofeu  37074  lineunray  37090  lineelsb2  37091  linethru  37096  mh-inf3sn  37508  unbdqndv2lem2  37554  knoppndvlem1  37556  knoppndvlem2  37557  knoppndvlem7  37562  knoppndvlem14  37569  bj-bary1lem  38423  bj-bary1lem1  38424  bj-bary1  38425  finxpreclem2  38505  finxp1o  38507  finxpreclem6  38511  fin2solem  38721  poimirlem9  38739  poimirlem15  38745  poimirlem20  38750  poimirlem24  38754  poimirlem25  38755  poimirlem27  38757  itg2addnclem2  38782  ftc1cnnc  38802  heibor1lem  38935  maxidln0  39171  lshpnelb  40233  lsatssn0  40251  lsatcv0  40280  lsat0cv  40282  lsatexch1  40295  l1cvat  40304  atlen0  40559  cvlsupr2  40592  atcvrj2b  40681  2atlt  40688  atbtwn  40695  3noncolr2  40698  4noncolr3  40702  3dimlem3  40710  3dimlem3OLDN  40711  3dimlem4  40713  3dimlem4OLDN  40714  3dim2  40717  1cvratex  40722  1cvrat  40725  ps-1  40726  ps-2  40727  hlatexch4  40730  3atlem4  40735  3atlem6  40737  4atlem0ae  40843  4atlem0be  40844  dalemccnedd  40936  dalemrotps  40940  dalem21  40943  dalem23  40945  dalem27  40948  dalem41  40962  dalem44  40965  dalem54  40975  lnatexN  41028  lnjatN  41029  llnexchb2lem  41117  llnexchb2  41118  lhpn0  41253  lhpexle3lem  41260  lhpmatb  41280  4atexlemswapqr  41312  4atexlemc  41318  4atexlemnclw  41319  4atexlemcnd  41321  4atexlemex4  41322  4atexlemex6  41323  4atex  41325  trlat  41418  trlval4  41437  cdlemc5  41444  cdlemd4  41450  cdlemd7  41453  cdlemd9  41455  cdleme0e  41466  cdleme3b  41478  cdleme3c  41479  cdleme3e  41481  cdleme3h  41484  cdleme7aa  41491  cdleme7e  41496  cdleme7ga  41497  cdleme9  41502  cdleme11c  41510  cdleme11e  41512  cdleme11fN  41513  cdleme11h  41515  cdleme11j  41516  cdleme11k  41517  cdleme15b  41524  cdleme15c  41525  cdleme17c  41537  cdleme18b  41541  cdlemesner  41545  cdleme20zN  41550  cdleme19c  41554  cdleme19d  41555  cdleme19e  41556  cdleme20m  41572  cdleme21a  41574  cdleme21b  41575  cdleme21c  41576  cdleme22f2  41596  cdleme28b  41620  cdleme36a  41709  cdleme36m  41710  cdleme41sn4aw  41724  cdleme43bN  41739  cdleme43dN  41741  cdleme46f2g2  41742  cdleme46f2g1  41743  cdleme4gfv  41756  cdlemeg46nlpq  41766  cdlemeg46req  41778  cdlemeg46fgN  41783  cdlemf1  41810  cdlemg8b  41877  cdlemg9a  41881  cdlemg12g  41898  cdlemg12  41899  cdlemg13a  41900  cdlemg17pq  41921  cdlemg18a  41927  cdlemg18c  41929  cdlemg19a  41932  cdlemg19  41933  cdlemg21  41935  cdlemg31b0N  41943  cdlemg31b0a  41944  cdlemg31c  41948  cdlemg33b0  41950  cdlemg33c0  41951  trlcone  41977  cdlemg42  41978  cdlemg44a  41980  cdlemg46  41984  cdlemh1  42064  cdlemh2  42065  cdlemh  42066  cdlemj3  42072  cdlemk3  42082  cdlemki  42090  cdlemksv2  42096  cdlemk12  42099  cdlemk14  42103  cdlemk15  42104  cdlemk7u  42119  cdlemk11u  42120  cdlemk12u  42121  cdlemk21N  42122  cdlemk20  42123  cdlemk22  42142  cdlemk26-3  42155  cdlemk27-3  42156  cdlemk28-3  42157  cdlemkfid3N  42174  cdlemk11ta  42178  cdlemk47  42198  cdlemk54  42207  dia2dimlem1  42313  dochsat  42632  dochshpncl  42633  lclkrlem2b  42757  lcfrlem21  42812  baerlem5amN  42965  baerlem5bmN  42966  baerlem5abmN  42967  mapdindp4  42972  mapdheq2  42978  mapdheq2biN  42979  mapdh6aN  42984  mapdh6dN  42988  mapdh6eN  42989  mapdh6hN  42992  mapdh7eN  42997  mapdh7dN  42999  mapdh7fN  43000  mapdh8ab  43026  mapdh8ad  43028  mapdh8e  43033  mapdh9a  43038  mapdh9aOLDN  43039  hdmap1l6a  43058  hdmap1l6d  43062  hdmap1l6e  43063  hdmap1l6h  43066  hdmap1eulem  43071  hdmap1eulemOLDN  43072  hdmapval0  43082  hdmapeveclem  43083  hdmapval3lemN  43086  hdmap10lem  43088  hdmap11lem1  43090  hdmaprnlem3N  43099  hdmaprnlem9N  43106  hdmaprnlem3eN  43107  fzne2d  43222  lcmineqlem11  43281  3lexlogpow5ineq1  43296  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq1  43300  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  dvrelog2b  43308  dvrelogpow2b  43310  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8d3  43328  aks4d1p8  43329  aks4d1p9  43330  fldhmf1  43332  aks6d1c2p2  43361  hashscontpow  43364  aks6d1c3  43365  aks6d1c5lem2  43380  2np3bcnp1  43386  2ap1caineq  43387  sticksstones1  43388  sticksstones2  43389  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem4  43415  aks6d1c7lem2  43423  unitscyglem2  43438  unitscyglem4  43440  aks5lem8  43443  xppss12  43476  mhpind  43815  jm2.26lem3  44201  rpnnen3lem  44231  rpnnen3  44232  imo72b2lem2  45359  imo72b2  45364  mnuprdlem1  45448  bcc0  45516  chordthmALT  46106  fnchoice  46251  refsum2cnlem1  46259  xrleneltd  46540  xrltned  46574  infleinf  46588  reclt0  46607  icoiccdif  46741  ressiooinf  46774  limcresiooub  46857  limcleqr  46859  limclner  46866  climxrre  46965  icccncfext  47102  cncfiooiccre  47110  dvnxpaek  47157  stoweidlem43  47258  stirlinglem5  47293  stirlinglem7  47295  dirkercncflem1  47318  fourierdlem24  47346  fourierdlem32  47354  fourierdlem33  47355  fourierdlem34  47356  fourierdlem35  47357  fourierdlem46  47367  fourierdlem48  47369  fourierdlem49  47370  fourierdlem64  47385  fourierdlem65  47386  fourierdlem74  47395  fourierdlem76  47397  fourierdlem79  47400  fourierdlem81  47402  fourierdlem91  47412  fourierdlem102  47423  fourierdlem114  47435  etransclem15  47464  etransclem24  47473  sge0rpcpnf  47636  sge0isum  47642  pimrecltpos  47923  sqrtnnaa  48118  m1modne  48629  minusmod5ne  48630  m1modnep2mod  48633  modmknepk  48643  modm2nep1  48647  modm1nep2  48649  setsnidel  48664  odz2prm2pw  48853  fmtnoprmfac1lem  48854  fmtnoprmfac1  48855  fmtnoprmfac2  48857  lighneallem1  48895  lighneallem3  48897  perfectALTVlem2  49025  usgrgrtrirex  49253  isubgr3stgrlem6  49274  gpgusgralem  49359  gpg3nbgrvtx0  49379  pgnioedg1  49411  pgnioedg2  49412  pgnioedg5  49415  nnsgrpnmnd  49480  smprngprmrng  49641  lvecpsslmod  49824  affinecomb1  50019  affinecomb2  50020  1subrec1sub  50022  rrx2plord2  50040  line  50050  rrxline  50052  eenglngeehlnmlem2  50056  rrx2vlinest  50058  line2xlem  50070  2itscp  50098