Theorem necomd 3012

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

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

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 2734

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

This theorem is used by:  difsnb  4772  0nelop  5477  xpdifid  6164  f1ounsn  7276  resf1extb  7934  difsnen  9060  fofinf1o  9302  en2eleq  10014  en2other2  10015  ackbij1lem15  10238  infpssrlem5  10312  fin23lem24  10327  fin23lem31  10348  isf32lem9  10366  canthnumlem  10660  canthp1lem2  10665  npomex  11008  ltned  11373  lt0ne0  11707  recgt0  12088  zneo  12707  xrltne  13216  supxrbnd  13382  flltnz  13874  seqf1olem1  14107  nn0opthi  14336  hashtpg  14552  hash7g  14553  hashge3el3dif  14554  cats1un  14792  sumtp  15837  geoserg  15957  geolim  15961  geolim2  15962  tanadd  16259  ruclem6  16327  ruclem7  16328  isprm2lem  16775  isprm5  16802  oddprm  16906  pcmpt  16988  cshwshashlem3  17193  resshom  17507  ressco  17508  mrissmrcd  17732  rescco  17925  estrres  18231  chnccat  18718  chnrev  18719  chnpof1  18722  smndex2dnrinv  19028  pmtrprfv  19581  symggen  19598  dprdcntz  20138  dprdres  20158  ablfac1b  20200  01eq0ringOLD  20693  nrhmzr  20700  zrdrng  20936  ornglmullt  21036  orngrmullt  21037  orngmullt  21038  ofldlt1  21042  lbspss  21267  lspsnnecom  21307  lspindp2l  21322  lspindp2  21323  islbs3  21343  lbsextlem4  21349  lidlnz  21440  isfieldidl  21450  qsidomlem2  21545  ssdifidlprm  21550  ofldchr  21790  uvcf1  22006  frlmup2  22013  psrridm  22178  coe1tmfv2  22502  coe1tmmul  22504  dmatmul  22720  mdetralt  22831  mdetunilem2  22836  mdetunilem6  22840  mdetunilem7  22841  maducoeval2  22863  madurid  22867  fvmptnn04ifa  23076  en2top  23211  cmpfi  23634  snfil  24091  tsmsfbas  24355  zcld  25041  iccpnfhmeo  25174  xrhmeo  25175  evth  25188  minveclem3b  25657  i1fres  25934  dvcnvlem  26205  ig1peu  26402  ig1pdvds  26407  aaliou3lem9  26583  taylthlem2  26607  abelthlem2  26665  abelthlem7  26671  cos02pilt1  26761  tanregt0  26774  logcj  26841  argimgt0  26847  dvloglem  26883  logf1o2  26885  logbrec  27017  ang180lem1  27044  ang180lem2  27045  ang180lem3  27046  ang180lem4  27047  ang180lem5  27048  ang180  27049  isosctrlem3  27055  ssscongptld  27057  affineequivne  27062  angpieqvdlem  27063  angpieqvdlem2  27064  angpieqvd  27066  chordthmlem  27067  chordthmlem2  27068  chordthm  27072  asinneg  27121  ppiltx  27411  perfectlem2  27464  lgsneg  27555  lgsqr  27585  lgseisenlem4  27612  lgsquadlem1  27614  lgsquadlem3  27616  lgsquad2  27620  2lgsoddprm  27650  dchrisum0flblem1  27742  noseponlem  27898  nosep1o  27915  nosep2o  27916  nosupbnd2lem1  27949  noinfbnd2lem1  27964  noetasuplem4  27970  noetainflem4  27974  lesrec  28062  0elright  28175  tgbtwnouttr  28837  tgifscgr  28848  tgcgrxfr  28858  tglngval  28891  tgfscgr  28908  tgbtwnconn1lem3  28914  tgbtwnconn3  28917  legtrid  28931  hltr  28953  hlbtwn  28954  btwnhl1  28955  btwnhl  28957  hlcgrex  28959  hlcgreulem  28960  lncom  28967  tgisline  28972  tglineeltr  28976  tglineelsb2  28977  tglinecom  28980  tglinethru  28981  ncolncol  28992  coltr  28993  coltr3  28994  tglnpt3  28999  tglnpt4  29000  symquadlem  29038  midexlem  29041  mirlni  29044  ragcol  29051  ragcgr  29059  perpneq  29066  footexALT  29070  footexlem1  29071  footexlem2  29072  foot  29074  footne  29075  colperpexlem3  29085  mideulem2  29087  opphllem  29088  midex  29090  opphllem1  29100  opphllem2  29101  opphllem3  29102  opphllem4  29103  opphllem5  29104  opphllem6  29105  outpasch  29110  hlpasch  29111  lnopp2hpgb  29118  colhp  29125  lnincplng  29139  plngrotlem1  29142  plngrotlem2  29143  plngrot  29145  lnssplnglem  29146  lnssplng  29147  lmieu  29166  hypcgrlem1  29182  hypcgrlem2  29183  lnperpex  29186  trgcopy  29188  trgcopyeulem  29189  iscgra1  29194  cgrane2  29197  cgrane3  29198  cgrane4  29199  cgracgr  29202  cgraid  29203  cgraswap  29204  cgrcgra  29205  cgracom  29206  cgratr  29207  zerocgra  29208  flatcgra  29209  cgraswaplr  29210  cgracol  29213  dfcgra2  29215  sacgr  29216  oacgr  29217  acopy  29218  acopyeu  29219  ragcgra  29220  ragsupplcgra  29222  ragraghl  29223  perpeqlem  29224  perpeq  29225  tgaaddcpbllem1  29226  tgaaddcpbllem2  29227  tgaaddcpbllem3  29228  tgaaddcpbl  29229  tgaaddcpbl2  29230  leagne2  29246  leagne3  29247  cgrg3col4  29249  angmndaddeu1  29252  angmndaddeu2  29253  angmndaddeu3  29254  angmndaddeu4  29255  angmndaddeu5  29256  angmndaddeu6  29257  angmndaddeu7  29258  angmndaddov1lem  29259  angmndaddov2lem  29260  angmndaddov1  29261  angmndaddov2  29262  angmndaddcpbl  29263  tgsas1  29264  tgsas2  29266  tgasa1  29268  dfprlng2  29290  dfprlng3  29291  perpprlng  29293  prlngex  29294  prlngmolem1  29295  prlngmolem2  29296  prlngmo2  29299  prlngmid2  29304  symquadprlng  29305  prlngsymquadlem  29306  prlngsymquadopp  29308  quadcgrprlng  29309  tgaltai  29310  ttgcontlem1  29327  brbtwn2  29348  axlowdimlem15  29399  axlowdimlem16  29400  axcontlem8  29414  upgrex  29535  edglnl  29586  umgrvad2edg  29659  nbupgr  29790  nbumgrvtx  29792  nbgr2vtx1edg  29796  nbuhgr2vtx1edgb  29798  nbupgrres  29810  cplgr3v  29881  cusgrexilem2  29888  usgredgsscusgredg  29905  1hegrvtxdg1r  29954  1egrvtxdg1r  29956  1egrvtxdg0  29957  pthdadjvtx  30178  pthdlem2lem  30218  wspniunwspnon  30377  umgr2cwwk2dif  30520  umgr2cycllem  30611  3pthdlem1  30630  uhgr3cyclex  30648  upgr4cycl4dv4e  30651  frgr3v  30741  1to3vfriswmgr  30746  frgrwopreglem5a  30777  frgrwopreglem3  30780  frgrhash2wsp  30798  staddi  32713  unidifsnne  32997  ifnefals  33009  coprprop  33158  sgnval2  33193  pmtrcnel  33516  pmtrcnel2  33517  psgnfzto1stlem  33527  cycpmco2lem1  33553  cycpmco2  33560  cyc2fvx  33561  cyc3co2  33567  cycpmrn  33570  tocyccntz  33571  cyc3evpm  33577  cyc3genpmlem  33578  isarchiofld  33626  drngidlhash  33848  mxidlnzr  33857  drng0mxidl  33865  drngmxidl  33866  qsdrng  33886  dflringlem3  33893  dflring3  33894  dflring4  33895  rsprprmprmidl  33919  deg1prod  33980  vietadeg1  34075  ply1annnr  34200  constrrtll  34228  constrrtlc1  34229  constrrtcclem  34231  constrrtcc  34232  constrfin  34243  constrelextdg2  34244  cos9thpiminplylem3  34281  1smat1  34301  submateqlem1  34304  ordtconnlem1  34421  esumrnmpt2  34565  cntnevol  34726  signstfveq0a  35071  repr0  35106  reprlt  35114  reprinfz1  35117  morleylemrneab  35166  nelscottrankgt  35619  cusgredgex  35707  2cycl2d  35713  acycgr1v  35715  derangenlem  35737  subfacp1lem1  35745  subfacp1lem3  35748  subfacp1lem5  35750  fmlasucdisj  35965  dfrdg4  36517  ifscgr  36611  cgrxfr  36622  btwnconn1lem8  36661  btwnconn3  36670  segcon2  36672  broutsideof3  36693  outsideoftr  36696  outsideofeq  36697  outsideofeu  36698  lineunray  36714  lineelsb2  36715  linethru  36720  mh-inf3f1  37147  mh-inf3sn  37148  unbdqndv2lem2  37194  knoppndvlem1  37196  knoppndvlem2  37197  knoppndvlem7  37202  knoppndvlem14  37209  bj-bary1lem  38049  bj-bary1lem1  38050  bj-bary1  38051  finxpreclem2  38131  finxp1o  38133  finxpreclem6  38137  fin2solem  38347  poimirlem9  38365  poimirlem15  38371  poimirlem20  38376  poimirlem24  38380  poimirlem25  38381  poimirlem27  38383  itg2addnclem2  38408  ftc1cnnc  38428  heibor1lem  38546  maxidln0  38782  lshpnelb  39844  lsatssn0  39862  lsatcv0  39891  lsat0cv  39893  lsatexch1  39906  l1cvat  39915  atlen0  40170  cvlsupr2  40203  atcvrj2b  40292  2atlt  40299  atbtwn  40306  3noncolr2  40309  4noncolr3  40313  3dimlem3  40321  3dimlem3OLDN  40322  3dimlem4  40324  3dimlem4OLDN  40325  3dim2  40328  1cvratex  40333  1cvrat  40336  ps-1  40337  ps-2  40338  hlatexch4  40341  3atlem4  40346  3atlem6  40348  4atlem0ae  40454  4atlem0be  40455  dalemccnedd  40547  dalemrotps  40551  dalem21  40554  dalem23  40556  dalem27  40559  dalem41  40573  dalem44  40576  dalem54  40586  lnatexN  40639  lnjatN  40640  llnexchb2lem  40728  llnexchb2  40729  lhpn0  40864  lhpexle3lem  40871  lhpmatb  40891  4atexlemswapqr  40923  4atexlemc  40929  4atexlemnclw  40930  4atexlemcnd  40932  4atexlemex4  40933  4atexlemex6  40934  4atex  40936  trlat  41029  trlval4  41048  cdlemc5  41055  cdlemd4  41061  cdlemd7  41064  cdlemd9  41066  cdleme0e  41077  cdleme3b  41089  cdleme3c  41090  cdleme3e  41092  cdleme3h  41095  cdleme7aa  41102  cdleme7e  41107  cdleme7ga  41108  cdleme9  41113  cdleme11c  41121  cdleme11e  41123  cdleme11fN  41124  cdleme11h  41126  cdleme11j  41127  cdleme11k  41128  cdleme15b  41135  cdleme15c  41136  cdleme17c  41148  cdleme18b  41152  cdlemesner  41156  cdleme20zN  41161  cdleme19c  41165  cdleme19d  41166  cdleme19e  41167  cdleme20m  41183  cdleme21a  41185  cdleme21b  41186  cdleme21c  41187  cdleme22f2  41207  cdleme28b  41231  cdleme36a  41320  cdleme36m  41321  cdleme41sn4aw  41335  cdleme43bN  41350  cdleme43dN  41352  cdleme46f2g2  41353  cdleme46f2g1  41354  cdleme4gfv  41367  cdlemeg46nlpq  41377  cdlemeg46req  41389  cdlemeg46fgN  41394  cdlemf1  41421  cdlemg8b  41488  cdlemg9a  41492  cdlemg12g  41509  cdlemg12  41510  cdlemg13a  41511  cdlemg17pq  41532  cdlemg18a  41538  cdlemg18c  41540  cdlemg19a  41543  cdlemg19  41544  cdlemg21  41546  cdlemg31b0N  41554  cdlemg31b0a  41555  cdlemg31c  41559  cdlemg33b0  41561  cdlemg33c0  41562  trlcone  41588  cdlemg42  41589  cdlemg44a  41591  cdlemg46  41595  cdlemh1  41675  cdlemh2  41676  cdlemh  41677  cdlemj3  41683  cdlemk3  41693  cdlemki  41701  cdlemksv2  41707  cdlemk12  41710  cdlemk14  41714  cdlemk15  41715  cdlemk7u  41730  cdlemk11u  41731  cdlemk12u  41732  cdlemk21N  41733  cdlemk20  41734  cdlemk22  41753  cdlemk26-3  41766  cdlemk27-3  41767  cdlemk28-3  41768  cdlemkfid3N  41785  cdlemk11ta  41789  cdlemk47  41809  cdlemk54  41818  dia2dimlem1  41924  dochsat  42243  dochshpncl  42244  lclkrlem2b  42368  lcfrlem21  42423  baerlem5amN  42576  baerlem5bmN  42577  baerlem5abmN  42578  mapdindp4  42583  mapdheq2  42589  mapdheq2biN  42590  mapdh6aN  42595  mapdh6dN  42599  mapdh6eN  42600  mapdh6hN  42603  mapdh7eN  42608  mapdh7dN  42610  mapdh7fN  42611  mapdh8ab  42637  mapdh8ad  42639  mapdh8e  42644  mapdh9a  42649  mapdh9aOLDN  42650  hdmap1l6a  42669  hdmap1l6d  42673  hdmap1l6e  42674  hdmap1l6h  42677  hdmap1eulem  42682  hdmap1eulemOLDN  42683  hdmapval0  42693  hdmapeveclem  42694  hdmapval3lemN  42697  hdmap10lem  42699  hdmap11lem1  42701  hdmaprnlem3N  42710  hdmaprnlem9N  42717  hdmaprnlem3eN  42718  fzne2d  42833  lcmineqlem11  42892  3lexlogpow5ineq1  42907  3lexlogpow5ineq2  42908  3lexlogpow5ineq4  42909  3lexlogpow5ineq3  42910  3lexlogpow2ineq1  42911  3lexlogpow2ineq2  42912  3lexlogpow5ineq5  42913  aks4d1lem1  42915  dvrelog2b  42919  dvrelogpow2b  42921  aks4d1p1p3  42922  aks4d1p1p2  42923  aks4d1p1p4  42924  aks4d1p1p6  42926  aks4d1p1p7  42927  aks4d1p1p5  42928  aks4d1p1  42929  aks4d1p2  42930  aks4d1p3  42931  aks4d1p5  42933  aks4d1p6  42934  aks4d1p7d1  42935  aks4d1p7  42936  aks4d1p8d3  42939  aks4d1p8  42940  aks4d1p9  42941  fldhmf1  42943  aks6d1c2p2  42972  hashscontpow  42975  aks6d1c3  42976  aks6d1c5lem2  42991  2np3bcnp1  42997  2ap1caineq  42998  sticksstones1  42999  sticksstones2  43000  sticksstones10  43008  sticksstones12a  43010  sticksstones12  43011  sticksstones22  43021  aks6d1c6lem4  43026  aks6d1c7lem2  43034  unitscyglem2  43049  unitscyglem4  43051  aks5lem8  43054  xppss12  43086  mhpind  43427  jm2.26lem3  43829  rpnnen3lem  43859  rpnnen3  43860  imo72b2lem2  44994  imo72b2  44999  mnuprdlem1  45083  bcc0  45151  chordthmALT  45742  fnchoice  45850  refsum2cnlem1  45858  xrleneltd  46140  xrltned  46174  infleinf  46188  reclt0  46207  icoiccdif  46341  ressiooinf  46374  limcresiooub  46457  limcleqr  46459  limclner  46466  climxrre  46565  icccncfext  46702  cncfiooiccre  46710  dvnxpaek  46757  stoweidlem43  46858  stirlinglem5  46893  stirlinglem7  46895  dirkercncflem1  46918  fourierdlem24  46946  fourierdlem32  46954  fourierdlem33  46955  fourierdlem34  46956  fourierdlem35  46957  fourierdlem46  46967  fourierdlem48  46969  fourierdlem49  46970  fourierdlem64  46985  fourierdlem65  46986  fourierdlem74  46995  fourierdlem76  46997  fourierdlem79  47000  fourierdlem81  47002  fourierdlem91  47012  fourierdlem102  47023  fourierdlem114  47035  etransclem15  47064  etransclem24  47073  sge0rpcpnf  47236  sge0isum  47242  pimrecltpos  47523  sqrtnnaa  47718  m1modne  48229  minusmod5ne  48230  m1modnep2mod  48233  modmknepk  48243  modm2nep1  48247  modm1nep2  48249  setsnidel  48264  odz2prm2pw  48453  fmtnoprmfac1lem  48454  fmtnoprmfac1  48455  fmtnoprmfac2  48457  lighneallem1  48495  lighneallem3  48497  perfectALTVlem2  48625  usgrgrtrirex  48853  isubgr3stgrlem6  48874  gpgusgralem  48959  gpg3nbgrvtx0  48979  pgnioedg1  49011  pgnioedg2  49012  pgnioedg5  49015  nnsgrpnmnd  49080  smprngprmrng  49241  lvecpsslmod  49424  affinecomb1  49619  affinecomb2  49620  1subrec1sub  49622  rrx2plord2  49639  line  49649  rrxline  49651  eenglngeehlnmlem2  49655  rrx2vlinest  49658  line2xlem  49670  2itscp  49698