Theorem necomd 2981

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

Syntax hints:   → wi 4   ≠ wne 2926

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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  difsnb  4773  0nelop  5459  xpdifid  6144  f1ounsn  7250  resf1extb  7913  difsnen  9027  fofinf1o  9290  en2eleq  9968  en2other2  9969  ackbij1lem15  10193  infpssrlem5  10267  fin23lem24  10282  fin23lem31  10303  isf32lem9  10321  canthnumlem  10608  canthp1lem2  10613  npomex  10956  ltned  11317  lt0ne0  11651  recgt0  12035  zneo  12624  xrltne  13130  supxrbnd  13295  flltnz  13780  seqf1olem1  14013  nn0opthi  14242  hashtpg  14457  hash7g  14458  hashge3el3dif  14459  cats1un  14693  sumtp  15722  geoserg  15839  geolim  15843  geolim2  15844  tanadd  16142  ruclem6  16210  ruclem7  16211  isprm2lem  16658  isprm5  16684  oddprm  16788  pcmpt  16870  cshwshashlem3  17075  resshom  17388  ressco  17389  mrissmrcd  17608  rescco  17801  estrres  18107  smndex2dnrinv  18849  pmtrprfv  19390  symggen  19407  dprdcntz  19947  dprdres  19967  ablfac1b  20009  01eq0ringOLD  20447  nrhmzr  20453  lbspss  20996  lspsnnecom  21036  lspindp2l  21051  lspindp2  21052  islbs3  21072  lbsextlem4  21078  lidlnz  21159  uvcf1  21708  frlmup2  21715  psrridm  21879  coe1tmfv2  22168  coe1tmmul  22170  dmatmul  22391  mdetralt  22502  mdetunilem2  22507  mdetunilem6  22511  mdetunilem7  22512  maducoeval2  22534  madurid  22538  fvmptnn04ifa  22744  en2top  22879  cmpfi  23302  snfil  23758  tsmsfbas  24022  zcld  24709  iccpnfhmeo  24850  xrhmeo  24851  evth  24865  minveclem3b  25335  i1fres  25613  dvcnvlem  25887  ig1peu  26087  ig1pdvds  26092  aaliou3lem9  26265  taylthlem2  26289  taylthlem2OLD  26290  abelthlem2  26349  abelthlem7  26355  cos02pilt1  26442  tanregt0  26455  logcj  26522  argimgt0  26528  dvloglem  26564  logf1o2  26566  logbrec  26699  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  ang180lem4  26729  ang180lem5  26730  ang180  26731  isosctrlem3  26737  ssscongptld  26739  affineequivne  26744  angpieqvdlem  26745  angpieqvdlem2  26746  angpieqvd  26748  chordthmlem  26749  chordthmlem2  26750  chordthm  26754  asinneg  26803  ppiltx  27094  perfectlem2  27148  lgsneg  27239  lgsqr  27269  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem3  27300  lgsquad2  27304  2lgsoddprm  27334  dchrisum0flblem1  27426  noseponlem  27583  nosep1o  27600  nosep2o  27601  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  slerec  27738  0elright  27830  tgbtwnouttr  28431  tgifscgr  28442  tgcgrxfr  28452  tglngval  28485  tgfscgr  28502  tgbtwnconn1lem3  28508  tgbtwnconn3  28511  legtrid  28525  hltr  28544  hlbtwn  28545  btwnhl1  28546  btwnhl  28548  hlcgrex  28550  hlcgreulem  28551  lncom  28556  tgisline  28561  tglineeltr  28565  tglineelsb2  28566  tglinecom  28569  tglinethru  28570  ncolncol  28580  coltr  28581  coltr3  28582  symquadlem  28623  midexlem  28626  ragcol  28633  ragcgr  28641  perpneq  28648  footexALT  28652  footexlem1  28653  footexlem2  28654  foot  28656  footne  28657  colperpexlem3  28666  mideulem2  28668  opphllem  28669  midex  28671  opphllem1  28681  opphllem2  28682  opphllem3  28683  opphllem4  28684  opphllem5  28685  opphllem6  28686  outpasch  28689  hlpasch  28690  lnopp2hpgb  28697  colhp  28704  lmieu  28718  hypcgrlem1  28733  hypcgrlem2  28734  lnperpex  28737  trgcopy  28738  trgcopyeulem  28739  iscgra1  28744  cgrane2  28747  cgrane3  28748  cgrane4  28749  cgracgr  28752  cgraid  28753  cgraswap  28754  cgrcgra  28755  cgracom  28756  cgratr  28757  flatcgra  28758  cgraswaplr  28759  cgracol  28762  dfcgra2  28764  sacgr  28765  oacgr  28766  acopy  28767  acopyeu  28768  leagne2  28784  leagne3  28785  cgrg3col4  28787  tgsas1  28788  tgsas2  28790  tgasa1  28792  ttgcontlem1  28819  brbtwn2  28839  axlowdimlem15  28890  axlowdimlem16  28891  axcontlem8  28905  upgrex  29026  edglnl  29077  umgrvad2edg  29147  nbupgr  29278  nbumgrvtx  29280  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  nbupgrres  29298  cplgr3v  29369  cusgrexilem2  29376  usgredgsscusgredg  29394  1hegrvtxdg1r  29443  1egrvtxdg1r  29445  1egrvtxdg0  29446  pthdadjvtx  29665  pthdlem2lem  29704  wspniunwspnon  29860  umgr2cwwk2dif  30000  3pthdlem1  30100  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  frgr3v  30211  1to3vfriswmgr  30216  frgrwopreglem5a  30247  frgrwopreglem3  30250  frgrhash2wsp  30268  staddi  32182  unidifsnne  32472  ifnefals  32484  coprprop  32629  sgnval2  32665  pmtrcnel  33053  pmtrcnel2  33054  psgnfzto1stlem  33064  cycpmco2lem1  33090  cycpmco2  33097  cyc2fvx  33098  cyc3co2  33104  cycpmrn  33107  tocyccntz  33108  cyc3evpm  33114  cyc3genpmlem  33115  ornglmullt  33292  orngrmullt  33293  orngmullt  33294  ofldlt1  33298  ofldchr  33299  isarchiofld  33302  drngidlhash  33412  qsidomlem2  33431  ssdifidlprm  33436  mxidlnzr  33445  drng0mxidl  33454  drngmxidl  33455  qsdrng  33475  rsprprmprmidl  33500  ply1annnr  33700  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  constrfin  33743  constrelextdg2  33744  cos9thpiminplylem3  33781  1smat1  33801  submateqlem1  33804  ordtconnlem1  33921  esumrnmpt2  34065  cntnevol  34225  signstfveq0a  34574  repr0  34609  reprlt  34617  reprinfz1  34620  cusgredgex  35116  2cycl2d  35133  acycgr1v  35143  derangenlem  35165  subfacp1lem1  35173  subfacp1lem3  35176  subfacp1lem5  35178  fmlasucdisj  35393  dfrdg4  35946  ifscgr  36039  cgrxfr  36050  btwnconn1lem8  36089  btwnconn3  36098  segcon2  36100  broutsideof3  36121  outsideoftr  36124  outsideofeq  36125  outsideofeu  36126  lineunray  36142  lineelsb2  36143  linethru  36148  unbdqndv2lem2  36505  knoppndvlem1  36507  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem14  36520  bj-bary1lem  37305  bj-bary1lem1  37306  bj-bary1  37307  finxpreclem2  37385  finxp1o  37387  finxpreclem6  37391  fin2solem  37607  poimirlem9  37630  poimirlem15  37636  poimirlem20  37641  poimirlem24  37645  poimirlem25  37646  poimirlem27  37648  itg2addnclem2  37673  ftc1cnnc  37693  heibor1lem  37810  maxidln0  38046  lshpnelb  38984  lsatssn0  39002  lsatcv0  39031  lsat0cv  39033  lsatexch1  39046  l1cvat  39055  atlen0  39310  cvlsupr2  39343  atcvrj2b  39433  2atlt  39440  atbtwn  39447  3noncolr2  39450  4noncolr3  39454  3dimlem3  39462  3dimlem3OLDN  39463  3dimlem4  39465  3dimlem4OLDN  39466  3dim2  39469  1cvratex  39474  1cvrat  39477  ps-1  39478  ps-2  39479  hlatexch4  39482  3atlem4  39487  3atlem6  39489  4atlem0ae  39595  4atlem0be  39596  dalemccnedd  39688  dalemrotps  39692  dalem21  39695  dalem23  39697  dalem27  39700  dalem41  39714  dalem44  39717  dalem54  39727  lnatexN  39780  lnjatN  39781  llnexchb2lem  39869  llnexchb2  39870  lhpn0  40005  lhpexle3lem  40012  lhpmatb  40032  4atexlemswapqr  40064  4atexlemc  40070  4atexlemnclw  40071  4atexlemcnd  40073  4atexlemex4  40074  4atexlemex6  40075  4atex  40077  trlat  40170  trlval4  40189  cdlemc5  40196  cdlemd4  40202  cdlemd7  40205  cdlemd9  40207  cdleme0e  40218  cdleme3b  40230  cdleme3c  40231  cdleme3e  40233  cdleme3h  40236  cdleme7aa  40243  cdleme7e  40248  cdleme7ga  40249  cdleme9  40254  cdleme11c  40262  cdleme11e  40264  cdleme11fN  40265  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme15b  40276  cdleme15c  40277  cdleme17c  40289  cdleme18b  40293  cdlemesner  40297  cdleme20zN  40302  cdleme19c  40306  cdleme19d  40307  cdleme19e  40308  cdleme20m  40324  cdleme21a  40326  cdleme21b  40327  cdleme21c  40328  cdleme22f2  40348  cdleme28b  40372  cdleme36a  40461  cdleme36m  40462  cdleme41sn4aw  40476  cdleme43bN  40491  cdleme43dN  40493  cdleme46f2g2  40494  cdleme46f2g1  40495  cdleme4gfv  40508  cdlemeg46nlpq  40518  cdlemeg46req  40530  cdlemeg46fgN  40535  cdlemf1  40562  cdlemg8b  40629  cdlemg9a  40633  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg17pq  40673  cdlemg18a  40679  cdlemg18c  40681  cdlemg19a  40684  cdlemg19  40685  cdlemg21  40687  cdlemg31b0N  40695  cdlemg31b0a  40696  cdlemg31c  40700  cdlemg33b0  40702  cdlemg33c0  40703  trlcone  40729  cdlemg42  40730  cdlemg44a  40732  cdlemg46  40736  cdlemh1  40816  cdlemh2  40817  cdlemh  40818  cdlemj3  40824  cdlemk3  40834  cdlemki  40842  cdlemksv2  40848  cdlemk12  40851  cdlemk14  40855  cdlemk15  40856  cdlemk7u  40871  cdlemk11u  40872  cdlemk12u  40873  cdlemk21N  40874  cdlemk20  40875  cdlemk22  40894  cdlemk26-3  40907  cdlemk27-3  40908  cdlemk28-3  40909  cdlemkfid3N  40926  cdlemk11ta  40930  cdlemk47  40950  cdlemk54  40959  dia2dimlem1  41065  dochsat  41384  dochshpncl  41385  lclkrlem2b  41509  lcfrlem21  41564  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdindp4  41724  mapdheq2  41730  mapdheq2biN  41731  mapdh6aN  41736  mapdh6dN  41740  mapdh6eN  41741  mapdh6hN  41744  mapdh7eN  41749  mapdh7dN  41751  mapdh7fN  41752  mapdh8ab  41778  mapdh8ad  41780  mapdh8e  41785  mapdh9a  41790  mapdh9aOLDN  41791  hdmap1l6a  41810  hdmap1l6d  41814  hdmap1l6e  41815  hdmap1l6h  41818  hdmap1eulem  41823  hdmap1eulemOLDN  41824  hdmapval0  41834  hdmapeveclem  41835  hdmapval3lemN  41838  hdmap10lem  41840  hdmap11lem1  41842  hdmaprnlem3N  41851  hdmaprnlem9N  41858  hdmaprnlem3eN  41859  fzne2d  41975  lcmineqlem11  42034  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1lem1  42057  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8d3  42081  aks4d1p8  42082  aks4d1p9  42083  fldhmf1  42085  aks6d1c2p2  42114  hashscontpow  42117  aks6d1c3  42118  aks6d1c5lem2  42133  2np3bcnp1  42139  2ap1caineq  42140  sticksstones1  42141  sticksstones2  42142  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem4  42168  aks6d1c7lem2  42176  unitscyglem2  42191  unitscyglem4  42193  aks5lem8  42196  xppss12  42224  mhpind  42589  jm2.26lem3  42997  rpnnen3lem  43027  rpnnen3  43028  imo72b2lem2  44163  imo72b2  44168  mnuprdlem1  44268  bcc0  44336  chordthmALT  44929  fnchoice  45030  refsum2cnlem1  45038  xrleneltd  45326  xrltned  45360  infleinf  45375  reclt0  45394  icoiccdif  45529  ressiooinf  45562  limcresiooub  45647  limcleqr  45649  limclner  45656  climxrre  45755  icccncfext  45892  cncfiooiccre  45900  dvnxpaek  45947  stoweidlem43  46048  stirlinglem5  46083  stirlinglem7  46085  dirkercncflem1  46108  fourierdlem24  46136  fourierdlem32  46144  fourierdlem33  46145  fourierdlem34  46146  fourierdlem35  46147  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem64  46175  fourierdlem65  46176  fourierdlem74  46185  fourierdlem76  46187  fourierdlem79  46190  fourierdlem81  46192  fourierdlem91  46202  fourierdlem102  46213  fourierdlem114  46225  etransclem15  46254  etransclem24  46263  sge0rpcpnf  46426  sge0isum  46432  pimrecltpos  46713  pimiooltgt  46715  m1modne  47353  minusmod5ne  47354  m1modnep2mod  47357  modmknepk  47367  modm2nep1  47371  modm1nep2  47373  setsnidel  47382  odz2prm2pw  47568  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  fmtnoprmfac2  47572  lighneallem1  47610  lighneallem3  47612  perfectALTVlem2  47727  usgrgrtrirex  47953  isubgr3stgrlem6  47974  gpgusgralem  48051  gpg3nbgrvtx0  48071  pgnioedg1  48102  pgnioedg2  48103  pgnioedg5  48106  nnsgrpnmnd  48170  lvecpsslmod  48500  affinecomb1  48695  affinecomb2  48696  1subrec1sub  48698  rrx2plord2  48715  line  48725  rrxline  48727  eenglngeehlnmlem2  48731  rrx2vlinest  48734  line2xlem  48746  2itscp  48774