Theorem necomd 2988

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

Syntax hints:   → wi 4   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  difsnb  4750  0nelop  5442  xpdifid  6124  f1ounsn  7218  resf1extb  7876  difsnen  8988  fofinf1o  9233  en2eleq  9919  en2other2  9920  ackbij1lem15  10144  infpssrlem5  10218  fin23lem24  10233  fin23lem31  10254  isf32lem9  10272  canthnumlem  10560  canthp1lem2  10565  npomex  10908  ltned  11270  lt0ne0  11604  recgt0  11988  zneo  12576  xrltne  13078  supxrbnd  13244  flltnz  13732  seqf1olem1  13965  nn0opthi  14194  hashtpg  14409  hash7g  14410  hashge3el3dif  14411  cats1un  14645  sumtp  15673  geoserg  15790  geolim  15794  geolim2  15795  tanadd  16093  ruclem6  16161  ruclem7  16162  isprm2lem  16609  isprm5  16635  oddprm  16739  pcmpt  16821  cshwshashlem3  17026  resshom  17339  ressco  17340  mrissmrcd  17564  rescco  17757  estrres  18063  chnccat  18550  chnrev  18551  chnpof1  18554  smndex2dnrinv  18844  pmtrprfv  19386  symggen  19403  dprdcntz  19943  dprdres  19963  ablfac1b  20005  01eq0ringOLD  20466  nrhmzr  20472  ornglmullt  20804  orngrmullt  20805  orngmullt  20806  ofldlt1  20810  lbspss  21036  lspsnnecom  21076  lspindp2l  21091  lspindp2  21092  islbs3  21112  lbsextlem4  21118  lidlnz  21199  ofldchr  21533  uvcf1  21749  frlmup2  21756  psrridm  21919  coe1tmfv2  22218  coe1tmmul  22220  dmatmul  22440  mdetralt  22551  mdetunilem2  22556  mdetunilem6  22560  mdetunilem7  22561  maducoeval2  22583  madurid  22587  fvmptnn04ifa  22793  en2top  22928  cmpfi  23351  snfil  23807  tsmsfbas  24071  zcld  24757  iccpnfhmeo  24890  xrhmeo  24891  evth  24904  minveclem3b  25373  i1fres  25650  dvcnvlem  25921  ig1peu  26121  ig1pdvds  26126  aaliou3lem9  26298  taylthlem2  26322  taylthlem2OLD  26323  abelthlem2  26382  abelthlem7  26388  cos02pilt1  26475  tanregt0  26488  logcj  26555  argimgt0  26561  dvloglem  26597  logf1o2  26599  logbrec  26732  ang180lem1  26759  ang180lem2  26760  ang180lem3  26761  ang180lem4  26762  ang180lem5  26763  ang180  26764  isosctrlem3  26770  ssscongptld  26772  affineequivne  26777  angpieqvdlem  26778  angpieqvdlem2  26779  angpieqvd  26781  chordthmlem  26782  chordthmlem2  26783  chordthm  26787  asinneg  26836  ppiltx  27127  perfectlem2  27181  lgsneg  27272  lgsqr  27302  lgseisenlem4  27329  lgsquadlem1  27331  lgsquadlem3  27333  lgsquad2  27337  2lgsoddprm  27367  dchrisum0flblem1  27459  noseponlem  27616  nosep1o  27633  nosep2o  27634  nosupbnd2lem1  27667  noinfbnd2lem1  27682  noetasuplem4  27688  noetainflem4  27692  lesrec  27779  0elright  27892  tgbtwnouttr  28553  tgifscgr  28564  tgcgrxfr  28574  tglngval  28607  tgfscgr  28624  tgbtwnconn1lem3  28630  tgbtwnconn3  28633  legtrid  28647  hltr  28666  hlbtwn  28667  btwnhl1  28668  btwnhl  28670  hlcgrex  28672  hlcgreulem  28673  lncom  28678  tgisline  28683  tglineeltr  28687  tglineelsb2  28688  tglinecom  28691  tglinethru  28692  ncolncol  28702  coltr  28703  coltr3  28704  symquadlem  28745  midexlem  28748  ragcol  28755  ragcgr  28763  perpneq  28770  footexALT  28774  footexlem1  28775  footexlem2  28776  foot  28778  footne  28779  colperpexlem3  28788  mideulem2  28790  opphllem  28791  midex  28793  opphllem1  28803  opphllem2  28804  opphllem3  28805  opphllem4  28806  opphllem5  28807  opphllem6  28808  outpasch  28811  hlpasch  28812  lnopp2hpgb  28819  colhp  28826  lmieu  28840  hypcgrlem1  28855  hypcgrlem2  28856  lnperpex  28859  trgcopy  28860  trgcopyeulem  28861  iscgra1  28866  cgrane2  28869  cgrane3  28870  cgrane4  28871  cgracgr  28874  cgraid  28875  cgraswap  28876  cgrcgra  28877  cgracom  28878  cgratr  28879  flatcgra  28880  cgraswaplr  28881  cgracol  28884  dfcgra2  28886  sacgr  28887  oacgr  28888  acopy  28889  acopyeu  28890  leagne2  28906  leagne3  28907  cgrg3col4  28909  tgsas1  28910  tgsas2  28912  tgasa1  28914  ttgcontlem1  28941  brbtwn2  28962  axlowdimlem15  29013  axlowdimlem16  29014  axcontlem8  29028  upgrex  29149  edglnl  29200  umgrvad2edg  29270  nbupgr  29401  nbumgrvtx  29403  nbgr2vtx1edg  29407  nbuhgr2vtx1edgb  29409  nbupgrres  29421  cplgr3v  29492  cusgrexilem2  29499  usgredgsscusgredg  29517  1hegrvtxdg1r  29566  1egrvtxdg1r  29568  1egrvtxdg0  29569  pthdadjvtx  29785  pthdlem2lem  29824  wspniunwspnon  29980  umgr2cwwk2dif  30123  3pthdlem1  30223  uhgr3cyclex  30241  upgr4cycl4dv4e  30244  frgr3v  30334  1to3vfriswmgr  30339  frgrwopreglem5a  30370  frgrwopreglem3  30373  frgrhash2wsp  30391  staddi  32306  unidifsnne  32595  ifnefals  32607  coprprop  32761  sgnval2  32797  pmtrcnel  33155  pmtrcnel2  33156  psgnfzto1stlem  33166  cycpmco2lem1  33192  cycpmco2  33199  cyc2fvx  33200  cyc3co2  33206  cycpmrn  33209  tocyccntz  33210  cyc3evpm  33216  cyc3genpmlem  33217  isarchiofld  33265  drngidlhash  33499  qsidomlem2  33518  ssdifidlprm  33523  mxidlnzr  33532  drng0mxidl  33541  drngmxidl  33542  qsdrng  33562  rsprprmprmidl  33587  deg1prod  33648  vietadeg1  33727  ply1annnr  33853  constrrtll  33881  constrrtlc1  33882  constrrtcclem  33884  constrrtcc  33885  constrfin  33896  constrelextdg2  33897  cos9thpiminplylem3  33934  1smat1  33954  submateqlem1  33957  ordtconnlem1  34074  esumrnmpt2  34218  cntnevol  34378  signstfveq0a  34726  repr0  34761  reprlt  34769  reprinfz1  34772  cusgredgex  35310  2cycl2d  35327  acycgr1v  35337  derangenlem  35359  subfacp1lem1  35367  subfacp1lem3  35370  subfacp1lem5  35372  fmlasucdisj  35587  dfrdg4  36139  ifscgr  36232  cgrxfr  36243  btwnconn1lem8  36282  btwnconn3  36291  segcon2  36293  broutsideof3  36314  outsideoftr  36317  outsideofeq  36318  outsideofeu  36319  lineunray  36335  lineelsb2  36336  linethru  36341  unbdqndv2lem2  36768  knoppndvlem1  36770  knoppndvlem2  36771  knoppndvlem7  36776  knoppndvlem14  36783  bj-bary1lem  37622  bj-bary1lem1  37623  bj-bary1  37624  finxpreclem2  37702  finxp1o  37704  finxpreclem6  37708  fin2solem  37918  poimirlem9  37941  poimirlem15  37947  poimirlem20  37952  poimirlem24  37956  poimirlem25  37957  poimirlem27  37959  itg2addnclem2  37984  ftc1cnnc  38004  heibor1lem  38121  maxidln0  38357  lshpnelb  39421  lsatssn0  39439  lsatcv0  39468  lsat0cv  39470  lsatexch1  39483  l1cvat  39492  atlen0  39747  cvlsupr2  39780  atcvrj2b  39869  2atlt  39876  atbtwn  39883  3noncolr2  39886  4noncolr3  39890  3dimlem3  39898  3dimlem3OLDN  39899  3dimlem4  39901  3dimlem4OLDN  39902  3dim2  39905  1cvratex  39910  1cvrat  39913  ps-1  39914  ps-2  39915  hlatexch4  39918  3atlem4  39923  3atlem6  39925  4atlem0ae  40031  4atlem0be  40032  dalemccnedd  40124  dalemrotps  40128  dalem21  40131  dalem23  40133  dalem27  40136  dalem41  40150  dalem44  40153  dalem54  40163  lnatexN  40216  lnjatN  40217  llnexchb2lem  40305  llnexchb2  40306  lhpn0  40441  lhpexle3lem  40448  lhpmatb  40468  4atexlemswapqr  40500  4atexlemc  40506  4atexlemnclw  40507  4atexlemcnd  40509  4atexlemex4  40510  4atexlemex6  40511  4atex  40513  trlat  40606  trlval4  40625  cdlemc5  40632  cdlemd4  40638  cdlemd7  40641  cdlemd9  40643  cdleme0e  40654  cdleme3b  40666  cdleme3c  40667  cdleme3e  40669  cdleme3h  40672  cdleme7aa  40679  cdleme7e  40684  cdleme7ga  40685  cdleme9  40690  cdleme11c  40698  cdleme11e  40700  cdleme11fN  40701  cdleme11h  40703  cdleme11j  40704  cdleme11k  40705  cdleme15b  40712  cdleme15c  40713  cdleme17c  40725  cdleme18b  40729  cdlemesner  40733  cdleme20zN  40738  cdleme19c  40742  cdleme19d  40743  cdleme19e  40744  cdleme20m  40760  cdleme21a  40762  cdleme21b  40763  cdleme21c  40764  cdleme22f2  40784  cdleme28b  40808  cdleme36a  40897  cdleme36m  40898  cdleme41sn4aw  40912  cdleme43bN  40927  cdleme43dN  40929  cdleme46f2g2  40930  cdleme46f2g1  40931  cdleme4gfv  40944  cdlemeg46nlpq  40954  cdlemeg46req  40966  cdlemeg46fgN  40971  cdlemf1  40998  cdlemg8b  41065  cdlemg9a  41069  cdlemg12g  41086  cdlemg12  41087  cdlemg13a  41088  cdlemg17pq  41109  cdlemg18a  41115  cdlemg18c  41117  cdlemg19a  41120  cdlemg19  41121  cdlemg21  41123  cdlemg31b0N  41131  cdlemg31b0a  41132  cdlemg31c  41136  cdlemg33b0  41138  cdlemg33c0  41139  trlcone  41165  cdlemg42  41166  cdlemg44a  41168  cdlemg46  41172  cdlemh1  41252  cdlemh2  41253  cdlemh  41254  cdlemj3  41260  cdlemk3  41270  cdlemki  41278  cdlemksv2  41284  cdlemk12  41287  cdlemk14  41291  cdlemk15  41292  cdlemk7u  41307  cdlemk11u  41308  cdlemk12u  41309  cdlemk21N  41310  cdlemk20  41311  cdlemk22  41330  cdlemk26-3  41343  cdlemk27-3  41344  cdlemk28-3  41345  cdlemkfid3N  41362  cdlemk11ta  41366  cdlemk47  41386  cdlemk54  41395  dia2dimlem1  41501  dochsat  41820  dochshpncl  41821  lclkrlem2b  41945  lcfrlem21  42000  baerlem5amN  42153  baerlem5bmN  42154  baerlem5abmN  42155  mapdindp4  42160  mapdheq2  42166  mapdheq2biN  42167  mapdh6aN  42172  mapdh6dN  42176  mapdh6eN  42177  mapdh6hN  42180  mapdh7eN  42185  mapdh7dN  42187  mapdh7fN  42188  mapdh8ab  42214  mapdh8ad  42216  mapdh8e  42221  mapdh9a  42226  mapdh9aOLDN  42227  hdmap1l6a  42246  hdmap1l6d  42250  hdmap1l6e  42251  hdmap1l6h  42254  hdmap1eulem  42259  hdmap1eulemOLDN  42260  hdmapval0  42270  hdmapeveclem  42271  hdmapval3lemN  42274  hdmap10lem  42276  hdmap11lem1  42278  hdmaprnlem3N  42287  hdmaprnlem9N  42294  hdmaprnlem3eN  42295  fzne2d  42411  lcmineqlem11  42470  3lexlogpow5ineq1  42485  3lexlogpow5ineq2  42486  3lexlogpow5ineq4  42487  3lexlogpow5ineq3  42488  3lexlogpow2ineq1  42489  3lexlogpow2ineq2  42490  3lexlogpow5ineq5  42491  aks4d1lem1  42493  dvrelog2b  42497  dvrelogpow2b  42499  aks4d1p1p3  42500  aks4d1p1p2  42501  aks4d1p1p4  42502  aks4d1p1p6  42504  aks4d1p1p7  42505  aks4d1p1p5  42506  aks4d1p1  42507  aks4d1p2  42508  aks4d1p3  42509  aks4d1p5  42511  aks4d1p6  42512  aks4d1p7d1  42513  aks4d1p7  42514  aks4d1p8d3  42517  aks4d1p8  42518  aks4d1p9  42519  fldhmf1  42521  aks6d1c2p2  42550  hashscontpow  42553  aks6d1c3  42554  aks6d1c5lem2  42569  2np3bcnp1  42575  2ap1caineq  42576  sticksstones1  42577  sticksstones2  42578  sticksstones10  42586  sticksstones12a  42588  sticksstones12  42589  sticksstones22  42599  aks6d1c6lem4  42604  aks6d1c7lem2  42612  unitscyglem2  42627  unitscyglem4  42629  aks5lem8  42632  xppss12  42662  mhpind  43026  jm2.26lem3  43432  rpnnen3lem  43462  rpnnen3  43463  imo72b2lem2  44597  imo72b2  44602  mnuprdlem1  44702  bcc0  44770  chordthmALT  45362  fnchoice  45463  refsum2cnlem1  45471  xrleneltd  45756  xrltned  45790  infleinf  45804  reclt0  45823  icoiccdif  45958  ressiooinf  45991  limcresiooub  46074  limcleqr  46076  limclner  46083  climxrre  46182  icccncfext  46319  cncfiooiccre  46327  dvnxpaek  46374  stoweidlem43  46475  stirlinglem5  46510  stirlinglem7  46512  dirkercncflem1  46535  fourierdlem24  46563  fourierdlem32  46571  fourierdlem33  46572  fourierdlem34  46573  fourierdlem35  46574  fourierdlem46  46584  fourierdlem48  46586  fourierdlem49  46587  fourierdlem64  46602  fourierdlem65  46603  fourierdlem74  46612  fourierdlem76  46614  fourierdlem79  46617  fourierdlem81  46619  fourierdlem91  46629  fourierdlem102  46640  fourierdlem114  46652  etransclem15  46681  etransclem24  46690  sge0rpcpnf  46853  sge0isum  46859  pimrecltpos  47140  m1modne  47782  minusmod5ne  47783  m1modnep2mod  47786  modmknepk  47796  modm2nep1  47800  modm1nep2  47802  setsnidel  47811  odz2prm2pw  47997  fmtnoprmfac1lem  47998  fmtnoprmfac1  47999  fmtnoprmfac2  48001  lighneallem1  48039  lighneallem3  48041  perfectALTVlem2  48156  usgrgrtrirex  48384  isubgr3stgrlem6  48405  gpgusgralem  48490  gpg3nbgrvtx0  48510  pgnioedg1  48542  pgnioedg2  48543  pgnioedg5  48546  nnsgrpnmnd  48612  lvecpsslmod  48941  affinecomb1  49136  affinecomb2  49137  1subrec1sub  49139  rrx2plord2  49156  line  49166  rrxline  49168  eenglngeehlnmlem2  49172  rrx2vlinest  49175  line2xlem  49187  2itscp  49215