Theorem necomd 2987

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

Syntax hints:   → wi 4   ≠ wne 2932

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  difsnb  4782  0nelop  5471  xpdifid  6157  f1ounsn  7264  resf1extb  7928  difsnen  9065  fofinf1o  9342  en2eleq  10020  en2other2  10021  ackbij1lem15  10245  infpssrlem5  10319  fin23lem24  10334  fin23lem31  10355  isf32lem9  10373  canthnumlem  10660  canthp1lem2  10665  npomex  11008  ltned  11369  lt0ne0  11701  recgt0  12085  zneo  12674  xrltne  13177  supxrbnd  13342  flltnz  13826  seqf1olem1  14057  nn0opthi  14286  hashtpg  14501  hash7g  14502  hashge3el3dif  14503  cats1un  14737  sumtp  15763  geoserg  15880  geolim  15884  geolim2  15885  tanadd  16183  ruclem6  16251  ruclem7  16252  isprm2lem  16698  isprm5  16724  oddprm  16828  pcmpt  16910  cshwshashlem3  17115  resshom  17430  ressco  17431  mrissmrcd  17650  rescco  17843  estrres  18149  smndex2dnrinv  18891  pmtrprfv  19432  symggen  19449  dprdcntz  19989  dprdres  20009  ablfac1b  20051  01eq0ringOLD  20489  nrhmzr  20495  lbspss  21038  lspsnnecom  21078  lspindp2l  21093  lspindp2  21094  islbs3  21114  lbsextlem4  21120  lidlnz  21201  uvcf1  21750  frlmup2  21757  psrridm  21921  coe1tmfv2  22210  coe1tmmul  22212  dmatmul  22433  mdetralt  22544  mdetunilem2  22549  mdetunilem6  22553  mdetunilem7  22554  maducoeval2  22576  madurid  22580  fvmptnn04ifa  22786  en2top  22921  cmpfi  23344  snfil  23800  tsmsfbas  24064  zcld  24751  iccpnfhmeo  24892  xrhmeo  24893  evth  24907  minveclem3b  25378  i1fres  25656  dvcnvlem  25930  ig1peu  26130  ig1pdvds  26135  aaliou3lem9  26308  taylthlem2  26332  taylthlem2OLD  26333  abelthlem2  26392  abelthlem7  26398  cos02pilt1  26485  tanregt0  26498  logcj  26565  argimgt0  26571  dvloglem  26607  logf1o2  26609  logbrec  26742  ang180lem1  26769  ang180lem2  26770  ang180lem3  26771  ang180lem4  26772  ang180lem5  26773  ang180  26774  isosctrlem3  26780  ssscongptld  26782  affineequivne  26787  angpieqvdlem  26788  angpieqvdlem2  26789  angpieqvd  26791  chordthmlem  26792  chordthmlem2  26793  chordthm  26797  asinneg  26846  ppiltx  27137  perfectlem2  27191  lgsneg  27282  lgsqr  27312  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem3  27343  lgsquad2  27347  2lgsoddprm  27377  dchrisum0flblem1  27469  noseponlem  27626  nosep1o  27643  nosep2o  27644  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noetasuplem4  27698  noetainflem4  27702  slerec  27781  0elright  27866  tgbtwnouttr  28422  tgifscgr  28433  tgcgrxfr  28443  tglngval  28476  tgfscgr  28493  tgbtwnconn1lem3  28499  tgbtwnconn3  28502  legtrid  28516  hltr  28535  hlbtwn  28536  btwnhl1  28537  btwnhl  28539  hlcgrex  28541  hlcgreulem  28542  lncom  28547  tgisline  28552  tglineeltr  28556  tglineelsb2  28557  tglinecom  28560  tglinethru  28561  ncolncol  28571  coltr  28572  coltr3  28573  symquadlem  28614  midexlem  28617  ragcol  28624  ragcgr  28632  perpneq  28639  footexALT  28643  footexlem1  28644  footexlem2  28645  foot  28647  footne  28648  colperpexlem3  28657  mideulem2  28659  opphllem  28660  midex  28662  opphllem1  28672  opphllem2  28673  opphllem3  28674  opphllem4  28675  opphllem5  28676  opphllem6  28677  outpasch  28680  hlpasch  28681  lnopp2hpgb  28688  colhp  28695  lmieu  28709  hypcgrlem1  28724  hypcgrlem2  28725  lnperpex  28728  trgcopy  28729  trgcopyeulem  28730  iscgra1  28735  cgrane2  28738  cgrane3  28739  cgrane4  28740  cgracgr  28743  cgraid  28744  cgraswap  28745  cgrcgra  28746  cgracom  28747  cgratr  28748  flatcgra  28749  cgraswaplr  28750  cgracol  28753  dfcgra2  28755  sacgr  28756  oacgr  28757  acopy  28758  acopyeu  28759  leagne2  28775  leagne3  28776  cgrg3col4  28778  tgsas1  28779  tgsas2  28781  tgasa1  28783  ttgcontlem1  28810  brbtwn2  28830  axlowdimlem15  28881  axlowdimlem16  28882  axcontlem8  28896  upgrex  29017  edglnl  29068  umgrvad2edg  29138  nbupgr  29269  nbumgrvtx  29271  nbgr2vtx1edg  29275  nbuhgr2vtx1edgb  29277  nbupgrres  29289  cplgr3v  29360  cusgrexilem2  29367  usgredgsscusgredg  29385  1hegrvtxdg1r  29434  1egrvtxdg1r  29436  1egrvtxdg0  29437  pthdadjvtx  29656  pthdlem2lem  29695  wspniunwspnon  29851  umgr2cwwk2dif  29991  3pthdlem1  30091  uhgr3cyclex  30109  upgr4cycl4dv4e  30112  frgr3v  30202  1to3vfriswmgr  30207  frgrwopreglem5a  30238  frgrwopreglem3  30241  frgrhash2wsp  30259  staddi  32173  unidifsnne  32463  ifnefals  32475  coprprop  32622  sgnval2  32658  pmtrcnel  33046  pmtrcnel2  33047  psgnfzto1stlem  33057  cycpmco2lem1  33083  cycpmco2  33090  cyc2fvx  33091  cyc3co2  33097  cycpmrn  33100  tocyccntz  33101  cyc3evpm  33107  cyc3genpmlem  33108  ornglmullt  33275  orngrmullt  33276  orngmullt  33277  ofldlt1  33281  ofldchr  33282  isarchiofld  33285  drngidlhash  33395  qsidomlem2  33414  ssdifidlprm  33419  mxidlnzr  33428  drng0mxidl  33437  drngmxidl  33438  qsdrng  33458  rsprprmprmidl  33483  ply1annnr  33683  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrfin  33726  constrelextdg2  33727  cos9thpiminplylem3  33764  1smat1  33781  submateqlem1  33784  ordtconnlem1  33901  esumrnmpt2  34045  cntnevol  34205  signstfveq0a  34554  repr0  34589  reprlt  34597  reprinfz1  34600  cusgredgex  35090  2cycl2d  35107  acycgr1v  35117  derangenlem  35139  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  fmlasucdisj  35367  dfrdg4  35915  ifscgr  36008  cgrxfr  36019  btwnconn1lem8  36058  btwnconn3  36067  segcon2  36069  broutsideof3  36090  outsideoftr  36093  outsideofeq  36094  outsideofeu  36095  lineunray  36111  lineelsb2  36112  linethru  36117  unbdqndv2lem2  36474  knoppndvlem1  36476  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem14  36489  bj-bary1lem  37274  bj-bary1lem1  37275  bj-bary1  37276  finxpreclem2  37354  finxp1o  37356  finxpreclem6  37360  fin2solem  37576  poimirlem9  37599  poimirlem15  37605  poimirlem20  37610  poimirlem24  37614  poimirlem25  37615  poimirlem27  37617  itg2addnclem2  37642  ftc1cnnc  37662  heibor1lem  37779  maxidln0  38015  lshpnelb  38948  lsatssn0  38966  lsatcv0  38995  lsat0cv  38997  lsatexch1  39010  l1cvat  39019  atlen0  39274  cvlsupr2  39307  atcvrj2b  39397  2atlt  39404  atbtwn  39411  3noncolr2  39414  4noncolr3  39418  3dimlem3  39426  3dimlem3OLDN  39427  3dimlem4  39429  3dimlem4OLDN  39430  3dim2  39433  1cvratex  39438  1cvrat  39441  ps-1  39442  ps-2  39443  hlatexch4  39446  3atlem4  39451  3atlem6  39453  4atlem0ae  39559  4atlem0be  39560  dalemccnedd  39652  dalemrotps  39656  dalem21  39659  dalem23  39661  dalem27  39664  dalem41  39678  dalem44  39681  dalem54  39691  lnatexN  39744  lnjatN  39745  llnexchb2lem  39833  llnexchb2  39834  lhpn0  39969  lhpexle3lem  39976  lhpmatb  39996  4atexlemswapqr  40028  4atexlemc  40034  4atexlemnclw  40035  4atexlemcnd  40037  4atexlemex4  40038  4atexlemex6  40039  4atex  40041  trlat  40134  trlval4  40153  cdlemc5  40160  cdlemd4  40166  cdlemd7  40169  cdlemd9  40171  cdleme0e  40182  cdleme3b  40194  cdleme3c  40195  cdleme3e  40197  cdleme3h  40200  cdleme7aa  40207  cdleme7e  40212  cdleme7ga  40213  cdleme9  40218  cdleme11c  40226  cdleme11e  40228  cdleme11fN  40229  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme15b  40240  cdleme15c  40241  cdleme17c  40253  cdleme18b  40257  cdlemesner  40261  cdleme20zN  40266  cdleme19c  40270  cdleme19d  40271  cdleme19e  40272  cdleme20m  40288  cdleme21a  40290  cdleme21b  40291  cdleme21c  40292  cdleme22f2  40312  cdleme28b  40336  cdleme36a  40425  cdleme36m  40426  cdleme41sn4aw  40440  cdleme43bN  40455  cdleme43dN  40457  cdleme46f2g2  40458  cdleme46f2g1  40459  cdleme4gfv  40472  cdlemeg46nlpq  40482  cdlemeg46req  40494  cdlemeg46fgN  40499  cdlemf1  40526  cdlemg8b  40593  cdlemg9a  40597  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg17pq  40637  cdlemg18a  40643  cdlemg18c  40645  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg31b0N  40659  cdlemg31b0a  40660  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33c0  40667  trlcone  40693  cdlemg42  40694  cdlemg44a  40696  cdlemg46  40700  cdlemh1  40780  cdlemh2  40781  cdlemh  40782  cdlemj3  40788  cdlemk3  40798  cdlemki  40806  cdlemksv2  40812  cdlemk12  40815  cdlemk14  40819  cdlemk15  40820  cdlemk7u  40835  cdlemk11u  40836  cdlemk12u  40837  cdlemk21N  40838  cdlemk20  40839  cdlemk22  40858  cdlemk26-3  40871  cdlemk27-3  40872  cdlemk28-3  40873  cdlemkfid3N  40890  cdlemk11ta  40894  cdlemk47  40914  cdlemk54  40923  dia2dimlem1  41029  dochsat  41348  dochshpncl  41349  lclkrlem2b  41473  lcfrlem21  41528  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdindp4  41688  mapdheq2  41694  mapdheq2biN  41695  mapdh6aN  41700  mapdh6dN  41704  mapdh6eN  41705  mapdh6hN  41708  mapdh7eN  41713  mapdh7dN  41715  mapdh7fN  41716  mapdh8ab  41742  mapdh8ad  41744  mapdh8e  41749  mapdh9a  41754  mapdh9aOLDN  41755  hdmap1l6a  41774  hdmap1l6d  41778  hdmap1l6e  41779  hdmap1l6h  41782  hdmap1eulem  41787  hdmap1eulemOLDN  41788  hdmapval0  41798  hdmapeveclem  41799  hdmapval3lemN  41802  hdmap10lem  41804  hdmap11lem1  41806  hdmaprnlem3N  41815  hdmaprnlem9N  41822  hdmaprnlem3eN  41823  fzne2d  41939  lcmineqlem11  41998  3lexlogpow5ineq1  42013  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq1  42017  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8d3  42045  aks4d1p8  42046  aks4d1p9  42047  fldhmf1  42049  aks6d1c2p2  42078  hashscontpow  42081  aks6d1c3  42082  aks6d1c5lem2  42097  2np3bcnp1  42103  2ap1caineq  42104  sticksstones1  42105  sticksstones2  42106  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem4  42132  aks6d1c7lem2  42140  unitscyglem2  42155  unitscyglem4  42157  aks5lem8  42160  metakunt7  42170  metakunt12  42175  metakunt22  42185  xppss12  42226  mhpind  42564  jm2.26lem3  42972  rpnnen3lem  43002  rpnnen3  43003  imo72b2lem2  44138  imo72b2  44143  mnuprdlem1  44244  bcc0  44312  chordthmALT  44905  fnchoice  45001  refsum2cnlem1  45009  xrleneltd  45298  xrltned  45332  infleinf  45347  reclt0  45366  icoiccdif  45501  ressiooinf  45534  limcresiooub  45619  limcleqr  45621  limclner  45628  climxrre  45727  icccncfext  45864  cncfiooiccre  45872  dvnxpaek  45919  stoweidlem43  46020  stirlinglem5  46055  stirlinglem7  46057  dirkercncflem1  46080  fourierdlem24  46108  fourierdlem32  46116  fourierdlem33  46117  fourierdlem34  46118  fourierdlem35  46119  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem64  46147  fourierdlem65  46148  fourierdlem74  46157  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem91  46174  fourierdlem102  46185  fourierdlem114  46197  etransclem15  46226  etransclem24  46235  sge0rpcpnf  46398  sge0isum  46404  pimrecltpos  46685  pimiooltgt  46687  m1modne  47325  minusmod5ne  47326  m1modnep2mod  47329  setsnidel  47339  odz2prm2pw  47525  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  fmtnoprmfac2  47529  lighneallem1  47567  lighneallem3  47569  perfectALTVlem2  47684  usgrgrtrirex  47910  isubgr3stgrlem6  47931  gpgusgralem  48008  gpg3nbgrvtx0  48026  gpg3nbgrvtx0ALT  48027  gpg3nbgrvtx1  48028  nnsgrpnmnd  48101  lvecpsslmod  48431  affinecomb1  48630  affinecomb2  48631  1subrec1sub  48633  rrx2plord2  48650  line  48660  rrxline  48662  eenglngeehlnmlem2  48666  rrx2vlinest  48669  line2xlem  48681  2itscp  48709