Theorem necomd 3010

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  difsnb  4768  0nelop  5467  xpdifid  6158  f1ounsn  7280  resf1extb  7946  difsnen  9078  fofinf1o  9321  en2eleq  10087  en2other2  10088  ackbij1lem15  10311  infpssrlem5  10385  fin23lem24  10400  fin23lem31  10421  isf32lem9  10439  canthnumlem  10733  canthp1lem2  10738  npomex  11081  ltned  11446  lt0ne0  11782  recgt0  12163  zneo  12782  xrltne  13292  supxrbnd  13458  flltnz  13951  seqf1olem1  14184  nn0opthi  14414  hashtpg  14630  hash7g  14631  hashge3el3dif  14632  cats1un  14870  sumtp  15915  geoserg  16035  geolim  16039  geolim2  16040  tanadd  16335  ruclem6  16403  ruclem7  16404  isprm2lem  16856  isprm5  16883  oddprm  16988  pcmpt  17070  cshwshashlem3  17275  resshom  17589  ressco  17590  mrissmrcd  17814  rescco  18007  estrres  18313  chnccat  18800  chnrev  18801  chnpof1  18804  smndex2dnrinv  19114  pmtrprfv  19667  symggen  19684  dprdcntz  20224  dprdres  20244  ablfac1b  20286  01eq0ringOLD  20782  nrhmzr  20789  zrdrng  21026  ornglmullt  21126  orngrmullt  21127  orngmullt  21128  ofldlt1  21132  lbspss  21357  lspsnnecom  21397  lspindp2l  21412  lspindp2  21413  islbs3  21433  lbsextlem4  21439  lidlnz  21530  isfieldidl  21540  qsidomlem2  21637  ssdifidlprm  21642  ofldchr  21882  uvcf1  22098  frlmup2  22105  psrridm  22270  coe1tmfv2  22594  coe1tmmul  22596  dmatmul  22812  mdetralt  22923  mdetunilem2  22928  mdetunilem6  22932  mdetunilem7  22933  maducoeval2  22955  madurid  22959  fvmptnn04ifa  23168  en2top  23303  cmpfi  23726  snfil  24183  tsmsfbas  24447  zcld  25133  iccpnfhmeo  25266  xrhmeo  25267  evth  25280  minveclem3b  25749  i1fres  26026  dvcnvlem  26296  ig1peu  26493  ig1pdvds  26498  aaliou3lem9  26677  taylthlem2  26701  abelthlem2  26759  abelthlem7  26765  cos02pilt1  26854  tanregt0  26867  logcj  26934  argimgt0  26940  dvloglem  26976  logf1o2  26978  logbrec  27110  ang180lem1  27137  ang180lem2  27138  ang180lem3  27139  ang180lem4  27140  ang180lem5  27141  ang180  27142  isosctrlem3  27148  ssscongptld  27150  affineequivne  27155  angpieqvdlem  27156  angpieqvdlem2  27157  angpieqvd  27159  chordthmlem  27160  chordthmlem2  27161  chordthm  27165  asinneg  27214  ppiltx  27504  perfectlem2  27557  lgsneg  27648  lgsqr  27678  lgseisenlem4  27705  lgsquadlem1  27707  lgsquadlem3  27709  lgsquad2  27713  2lgsoddprm  27743  dchrisum0flblem1  27835  noseponlem  28021  nosep1o  28038  nosep2o  28039  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetasuplem4  28093  noetainflem4  28097  lesrec  28185  0elright  28298  tgbtwnouttr  28960  tgifscgr  28971  tgcgrxfr  28981  tglngval  29014  tgfscgr  29031  tgbtwnconn1lem3  29037  tgbtwnconn3  29040  legtrid  29054  hltr  29076  hlbtwn  29077  btwnhl1  29078  btwnhl  29080  hlcgrex  29082  hlcgreulem  29083  lncom  29090  tgisline  29095  tglineeltr  29099  tglineelsb2  29100  tglinecom  29103  tglinethru  29104  ncolncol  29115  coltr  29116  coltr3  29117  tglnpt3  29122  tglnpt4  29123  symquadlem  29161  midexlem  29164  mirlni  29167  ragcol  29174  ragcgr  29182  perpneq  29189  footexALT  29193  footexlem1  29194  footexlem2  29195  foot  29197  footne  29198  colperpexlem3  29208  mideulem2  29210  opphllem  29211  midex  29213  opphllem1  29223  opphllem2  29224  opphllem3  29225  opphllem4  29226  opphllem5  29227  opphllem6  29228  outpasch  29233  hlpasch  29234  lnopp2hpgb  29241  colhp  29248  lnincplng  29262  plngrotlem1  29265  plngrotlem2  29266  plngrot  29268  lnssplnglem  29269  lnssplng  29270  lmieu  29289  hypcgrlem1  29305  hypcgrlem2  29306  lnperpex  29309  trgcopy  29311  trgcopyeulem  29312  iscgra1  29317  cgrane2  29320  cgrane3  29321  cgrane4  29322  cgracgr  29325  cgraid  29326  cgraswap  29327  cgrcgra  29328  cgracom  29329  cgratr  29330  zerocgra  29331  flatcgra  29332  cgraswaplr  29333  cgracol  29336  dfcgra2  29338  sacgr  29339  oacgr  29340  acopy  29341  acopyeu  29342  ragcgra  29343  ragsupplcgra  29345  ragraghl  29346  perpeqlem  29347  perpeq  29348  tgaaddcpbllem1  29349  tgaaddcpbllem2  29350  tgaaddcpbllem3  29351  tgaaddcpbl  29352  tgaaddcpbl2  29353  leagne2  29369  leagne3  29370  cgrg3col4  29372  cgrabasimass  29378  angmgmaddeu1  29379  angmgmaddeu2  29380  angmgmaddeu3  29381  angmgmaddeu4  29382  angmgmaddeu5  29383  angmgmaddeu6  29384  angmgmaddeu7  29385  angmgmaddov1lem  29386  angmgmaddov2lem  29387  angmgmaddov1  29388  angmgmaddov2  29389  angmgmaddcpbl  29390  angmgmaddcl  29391  angmgmaddlid  29392  angmgmaddrid  29393  angmgmlem  29395  angmgm  29397  tgsas1  29399  tgsas2  29401  tgasa1  29403  dfprlng2  29425  dfprlng3  29426  perpprlng  29428  prlngex  29429  prlngmolem1  29430  prlngmolem2  29431  prlngmo2  29434  prlngmid2  29439  symquadprlng  29440  prlngsymquadlem  29441  prlngsymquadopp  29443  quadcgrprlng  29444  tgaltai  29445  ttgcontlem1  29462  brbtwn2  29483  axlowdimlem15  29534  axlowdimlem16  29535  axcontlem8  29549  upgrex  29670  edglnl  29721  umgrvad2edg  29794  nbupgr  29925  nbumgrvtx  29927  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  nbupgrres  29945  cplgr3v  30016  cusgrexilem2  30023  usgredgsscusgredg  30040  1hegrvtxdg1r  30089  1egrvtxdg1r  30091  1egrvtxdg0  30092  pthdadjvtx  30313  pthdlem2lem  30353  wspniunwspnon  30512  umgr2cwwk2dif  30655  umgr2cycllem  30746  3pthdlem1  30765  uhgr3cyclex  30783  upgr4cycl4dv4e  30786  frgr3v  30876  1to3vfriswmgr  30881  frgrwopreglem5a  30912  frgrwopreglem3  30915  frgrhash2wsp  30933  staddi  32848  cgrahlb  33047  inagbtwn  33048  inagcgrasubhl  33049  inagcgrasubbtwn  33050  inagcgrabtwn  33051  inagcgratrgmain  33054  inaglea  33059  tgmircgra  33066  tgextancd  33068  tgextahpl  33069  tgextalem1inag  33070  tgextamirnhl  33072  tgextancgra  33074  tgextalt1  33076  tgextalt2  33077  tgexta  33078  tgaasncol  33080  tgaasexc  33081  tgaasne  33082  tgaascgra  33083  tgaas1  33085  unidifsnne  33174  ifnefals  33186  coprprop  33334  sgnval2  33369  pmtrcnel  33692  pmtrcnel2  33693  psgnfzto1stlem  33703  cycpmco2lem1  33729  cycpmco2  33736  cyc2fvx  33737  cyc3co2  33743  cycpmrn  33746  tocyccntz  33747  cyc3evpm  33753  cyc3genpmlem  33754  isarchiofld  33802  drngidlhash  34025  mxidlnzr  34034  drng0mxidl  34042  drngmxidl  34043  qsdrng  34063  dflringlem3  34070  dflring3  34071  dflring4  34072  rsprprmprmidl  34096  deg1prod  34157  vietadeg1  34252  ply1annnr  34377  constrrtll  34405  constrrtlc1  34406  constrrtcclem  34408  constrrtcc  34409  constrfin  34420  constrelextdg2  34421  cos9thpiminplylem3  34458  1smat1  34478  submateqlem1  34481  ordtconnlem1  34598  esumrnmpt2  34742  cntnevol  34903  signstfveq0a  35247  repr0  35282  reprlt  35290  reprinfz1  35293  morleylemrneab  35342  nelscottrankgt  35791  cusgredgex  35948  2cycl2d  35954  acycgr1v  35956  derangenlem  35978  subfacp1lem1  35986  subfacp1lem3  35989  subfacp1lem5  35991  fmlasucdisj  36206  dfrdg4  36757  ifscgr  36851  cgrxfr  36862  btwnconn1lem8  36901  btwnconn3  36910  segcon2  36912  broutsideof3  36933  outsideoftr  36936  outsideofeq  36937  outsideofeu  36938  lineunray  36954  lineelsb2  36955  linethru  36960  mh-inf3sn  37372  unbdqndv2lem2  37418  knoppndvlem1  37420  knoppndvlem2  37421  knoppndvlem7  37426  knoppndvlem14  37433  bj-bary1lem  38274  bj-bary1lem1  38275  bj-bary1  38276  finxpreclem2  38356  finxp1o  38358  finxpreclem6  38362  fin2solem  38572  poimirlem9  38590  poimirlem15  38596  poimirlem20  38601  poimirlem24  38605  poimirlem25  38606  poimirlem27  38608  itg2addnclem2  38633  ftc1cnnc  38653  heibor1lem  38786  maxidln0  39022  lshpnelb  40084  lsatssn0  40102  lsatcv0  40131  lsat0cv  40133  lsatexch1  40146  l1cvat  40155  atlen0  40410  cvlsupr2  40443  atcvrj2b  40532  2atlt  40539  atbtwn  40546  3noncolr2  40549  4noncolr3  40553  3dimlem3  40561  3dimlem3OLDN  40562  3dimlem4  40564  3dimlem4OLDN  40565  3dim2  40568  1cvratex  40573  1cvrat  40576  ps-1  40577  ps-2  40578  hlatexch4  40581  3atlem4  40586  3atlem6  40588  4atlem0ae  40694  4atlem0be  40695  dalemccnedd  40787  dalemrotps  40791  dalem21  40794  dalem23  40796  dalem27  40799  dalem41  40813  dalem44  40816  dalem54  40826  lnatexN  40879  lnjatN  40880  llnexchb2lem  40968  llnexchb2  40969  lhpn0  41104  lhpexle3lem  41111  lhpmatb  41131  4atexlemswapqr  41163  4atexlemc  41169  4atexlemnclw  41170  4atexlemcnd  41172  4atexlemex4  41173  4atexlemex6  41174  4atex  41176  trlat  41269  trlval4  41288  cdlemc5  41295  cdlemd4  41301  cdlemd7  41304  cdlemd9  41306  cdleme0e  41317  cdleme3b  41329  cdleme3c  41330  cdleme3e  41332  cdleme3h  41335  cdleme7aa  41342  cdleme7e  41347  cdleme7ga  41348  cdleme9  41353  cdleme11c  41361  cdleme11e  41363  cdleme11fN  41364  cdleme11h  41366  cdleme11j  41367  cdleme11k  41368  cdleme15b  41375  cdleme15c  41376  cdleme17c  41388  cdleme18b  41392  cdlemesner  41396  cdleme20zN  41401  cdleme19c  41405  cdleme19d  41406  cdleme19e  41407  cdleme20m  41423  cdleme21a  41425  cdleme21b  41426  cdleme21c  41427  cdleme22f2  41447  cdleme28b  41471  cdleme36a  41560  cdleme36m  41561  cdleme41sn4aw  41575  cdleme43bN  41590  cdleme43dN  41592  cdleme46f2g2  41593  cdleme46f2g1  41594  cdleme4gfv  41607  cdlemeg46nlpq  41617  cdlemeg46req  41629  cdlemeg46fgN  41634  cdlemf1  41661  cdlemg8b  41728  cdlemg9a  41732  cdlemg12g  41749  cdlemg12  41750  cdlemg13a  41751  cdlemg17pq  41772  cdlemg18a  41778  cdlemg18c  41780  cdlemg19a  41783  cdlemg19  41784  cdlemg21  41786  cdlemg31b0N  41794  cdlemg31b0a  41795  cdlemg31c  41799  cdlemg33b0  41801  cdlemg33c0  41802  trlcone  41828  cdlemg42  41829  cdlemg44a  41831  cdlemg46  41835  cdlemh1  41915  cdlemh2  41916  cdlemh  41917  cdlemj3  41923  cdlemk3  41933  cdlemki  41941  cdlemksv2  41947  cdlemk12  41950  cdlemk14  41954  cdlemk15  41955  cdlemk7u  41970  cdlemk11u  41971  cdlemk12u  41972  cdlemk21N  41973  cdlemk20  41974  cdlemk22  41993  cdlemk26-3  42006  cdlemk27-3  42007  cdlemk28-3  42008  cdlemkfid3N  42025  cdlemk11ta  42029  cdlemk47  42049  cdlemk54  42058  dia2dimlem1  42164  dochsat  42483  dochshpncl  42484  lclkrlem2b  42608  lcfrlem21  42663  baerlem5amN  42816  baerlem5bmN  42817  baerlem5abmN  42818  mapdindp4  42823  mapdheq2  42829  mapdheq2biN  42830  mapdh6aN  42835  mapdh6dN  42839  mapdh6eN  42840  mapdh6hN  42843  mapdh7eN  42848  mapdh7dN  42850  mapdh7fN  42851  mapdh8ab  42877  mapdh8ad  42879  mapdh8e  42884  mapdh9a  42889  mapdh9aOLDN  42890  hdmap1l6a  42909  hdmap1l6d  42913  hdmap1l6e  42914  hdmap1l6h  42917  hdmap1eulem  42922  hdmap1eulemOLDN  42923  hdmapval0  42933  hdmapeveclem  42934  hdmapval3lemN  42937  hdmap10lem  42939  hdmap11lem1  42941  hdmaprnlem3N  42950  hdmaprnlem9N  42957  hdmaprnlem3eN  42958  fzne2d  43073  lcmineqlem11  43132  3lexlogpow5ineq1  43147  3lexlogpow5ineq2  43148  3lexlogpow5ineq4  43149  3lexlogpow5ineq3  43150  3lexlogpow2ineq1  43151  3lexlogpow2ineq2  43152  3lexlogpow5ineq5  43153  aks4d1lem1  43155  dvrelog2b  43159  dvrelogpow2b  43161  aks4d1p1p3  43162  aks4d1p1p2  43163  aks4d1p1p4  43164  aks4d1p1p6  43166  aks4d1p1p7  43167  aks4d1p1p5  43168  aks4d1p1  43169  aks4d1p2  43170  aks4d1p3  43171  aks4d1p5  43173  aks4d1p6  43174  aks4d1p7d1  43175  aks4d1p7  43176  aks4d1p8d3  43179  aks4d1p8  43180  aks4d1p9  43181  fldhmf1  43183  aks6d1c2p2  43212  hashscontpow  43215  aks6d1c3  43216  aks6d1c5lem2  43231  2np3bcnp1  43237  2ap1caineq  43238  sticksstones1  43239  sticksstones2  43240  sticksstones10  43248  sticksstones12a  43250  sticksstones12  43251  sticksstones22  43261  aks6d1c6lem4  43266  aks6d1c7lem2  43274  unitscyglem2  43289  unitscyglem4  43291  aks5lem8  43294  xppss12  43326  mhpind  43665  jm2.26lem3  44051  rpnnen3lem  44081  rpnnen3  44082  imo72b2lem2  45210  imo72b2  45215  mnuprdlem1  45299  bcc0  45367  chordthmALT  45958  fnchoice  46089  refsum2cnlem1  46097  xrleneltd  46378  xrltned  46412  infleinf  46426  reclt0  46445  icoiccdif  46579  ressiooinf  46612  limcresiooub  46695  limcleqr  46697  limclner  46704  climxrre  46803  icccncfext  46940  cncfiooiccre  46948  dvnxpaek  46995  stoweidlem43  47096  stirlinglem5  47131  stirlinglem7  47133  dirkercncflem1  47156  fourierdlem24  47184  fourierdlem32  47192  fourierdlem33  47193  fourierdlem34  47194  fourierdlem35  47195  fourierdlem46  47205  fourierdlem48  47207  fourierdlem49  47208  fourierdlem64  47223  fourierdlem65  47224  fourierdlem74  47233  fourierdlem76  47235  fourierdlem79  47238  fourierdlem81  47240  fourierdlem91  47250  fourierdlem102  47261  fourierdlem114  47273  etransclem15  47302  etransclem24  47311  sge0rpcpnf  47474  sge0isum  47480  pimrecltpos  47761  sqrtnnaa  47956  m1modne  48467  minusmod5ne  48468  m1modnep2mod  48471  modmknepk  48481  modm2nep1  48485  modm1nep2  48487  setsnidel  48502  odz2prm2pw  48691  fmtnoprmfac1lem  48692  fmtnoprmfac1  48693  fmtnoprmfac2  48695  lighneallem1  48733  lighneallem3  48735  perfectALTVlem2  48863  usgrgrtrirex  49091  isubgr3stgrlem6  49112  gpgusgralem  49197  gpg3nbgrvtx0  49217  pgnioedg1  49249  pgnioedg2  49250  pgnioedg5  49253  nnsgrpnmnd  49318  smprngprmrng  49479  lvecpsslmod  49662  affinecomb1  49857  affinecomb2  49858  1subrec1sub  49860  rrx2plord2  49877  line  49887  rrxline  49889  eenglngeehlnmlem2  49893  rrx2vlinest  49896  line2xlem  49908  2itscp  49936