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  4763  0nelop  5445  xpdifid  6127  f1ounsn  7220  resf1extb  7878  difsnen  8991  fofinf1o  9236  en2eleq  9922  en2other2  9923  ackbij1lem15  10147  infpssrlem5  10221  fin23lem24  10236  fin23lem31  10257  isf32lem9  10275  canthnumlem  10563  canthp1lem2  10568  npomex  10911  ltned  11273  lt0ne0  11607  recgt0  11991  zneo  12579  xrltne  13081  supxrbnd  13247  flltnz  13735  seqf1olem1  13968  nn0opthi  14197  hashtpg  14412  hash7g  14413  hashge3el3dif  14414  cats1un  14648  sumtp  15676  geoserg  15793  geolim  15797  geolim2  15798  tanadd  16096  ruclem6  16164  ruclem7  16165  isprm2lem  16612  isprm5  16638  oddprm  16742  pcmpt  16824  cshwshashlem3  17029  resshom  17342  ressco  17343  mrissmrcd  17567  rescco  17760  estrres  18066  chnccat  18553  chnrev  18554  chnpof1  18557  smndex2dnrinv  18844  pmtrprfv  19386  symggen  19403  dprdcntz  19943  dprdres  19963  ablfac1b  20005  01eq0ringOLD  20468  nrhmzr  20474  ornglmullt  20806  orngrmullt  20807  orngmullt  20808  ofldlt1  20812  lbspss  21038  lspsnnecom  21078  lspindp2l  21093  lspindp2  21094  islbs3  21114  lbsextlem4  21120  lidlnz  21201  ofldchr  21535  uvcf1  21751  frlmup2  21758  psrridm  21922  coe1tmfv2  22221  coe1tmmul  22223  dmatmul  22445  mdetralt  22556  mdetunilem2  22561  mdetunilem6  22565  mdetunilem7  22566  maducoeval2  22588  madurid  22592  fvmptnn04ifa  22798  en2top  22933  cmpfi  23356  snfil  23812  tsmsfbas  24076  zcld  24762  iccpnfhmeo  24903  xrhmeo  24904  evth  24918  minveclem3b  25388  i1fres  25666  dvcnvlem  25940  ig1peu  26140  ig1pdvds  26145  aaliou3lem9  26318  taylthlem2  26342  taylthlem2OLD  26343  abelthlem2  26402  abelthlem7  26408  cos02pilt1  26495  tanregt0  26508  logcj  26575  argimgt0  26581  dvloglem  26617  logf1o2  26619  logbrec  26752  ang180lem1  26779  ang180lem2  26780  ang180lem3  26781  ang180lem4  26782  ang180lem5  26783  ang180  26784  isosctrlem3  26790  ssscongptld  26792  affineequivne  26797  angpieqvdlem  26798  angpieqvdlem2  26799  angpieqvd  26801  chordthmlem  26802  chordthmlem2  26803  chordthm  26807  asinneg  26856  ppiltx  27147  perfectlem2  27201  lgsneg  27292  lgsqr  27322  lgseisenlem4  27349  lgsquadlem1  27351  lgsquadlem3  27353  lgsquad2  27357  2lgsoddprm  27387  dchrisum0flblem1  27479  noseponlem  27636  nosep1o  27653  nosep2o  27654  nosupbnd2lem1  27687  noinfbnd2lem1  27702  noetasuplem4  27708  noetainflem4  27712  slerec  27797  0elright  27894  tgbtwnouttr  28552  tgifscgr  28563  tgcgrxfr  28573  tglngval  28606  tgfscgr  28623  tgbtwnconn1lem3  28629  tgbtwnconn3  28632  legtrid  28646  hltr  28665  hlbtwn  28666  btwnhl1  28667  btwnhl  28669  hlcgrex  28671  hlcgreulem  28672  lncom  28677  tgisline  28682  tglineeltr  28686  tglineelsb2  28687  tglinecom  28690  tglinethru  28691  ncolncol  28701  coltr  28702  coltr3  28703  symquadlem  28744  midexlem  28747  ragcol  28754  ragcgr  28762  perpneq  28769  footexALT  28773  footexlem1  28774  footexlem2  28775  foot  28777  footne  28778  colperpexlem3  28787  mideulem2  28789  opphllem  28790  midex  28792  opphllem1  28802  opphllem2  28803  opphllem3  28804  opphllem4  28805  opphllem5  28806  opphllem6  28807  outpasch  28810  hlpasch  28811  lnopp2hpgb  28818  colhp  28825  lmieu  28839  hypcgrlem1  28854  hypcgrlem2  28855  lnperpex  28858  trgcopy  28859  trgcopyeulem  28860  iscgra1  28865  cgrane2  28868  cgrane3  28869  cgrane4  28870  cgracgr  28873  cgraid  28874  cgraswap  28875  cgrcgra  28876  cgracom  28877  cgratr  28878  flatcgra  28879  cgraswaplr  28880  cgracol  28883  dfcgra2  28885  sacgr  28886  oacgr  28887  acopy  28888  acopyeu  28889  leagne2  28905  leagne3  28906  cgrg3col4  28908  tgsas1  28909  tgsas2  28911  tgasa1  28913  ttgcontlem1  28940  brbtwn2  28961  axlowdimlem15  29012  axlowdimlem16  29013  axcontlem8  29027  upgrex  29148  edglnl  29199  umgrvad2edg  29269  nbupgr  29400  nbumgrvtx  29402  nbgr2vtx1edg  29406  nbuhgr2vtx1edgb  29408  nbupgrres  29420  cplgr3v  29491  cusgrexilem2  29498  usgredgsscusgredg  29516  1hegrvtxdg1r  29565  1egrvtxdg1r  29567  1egrvtxdg0  29568  pthdadjvtx  29784  pthdlem2lem  29823  wspniunwspnon  29979  umgr2cwwk2dif  30122  3pthdlem1  30222  uhgr3cyclex  30240  upgr4cycl4dv4e  30243  frgr3v  30333  1to3vfriswmgr  30338  frgrwopreglem5a  30369  frgrwopreglem3  30372  frgrhash2wsp  30390  staddi  32304  unidifsnne  32593  ifnefals  32605  coprprop  32759  sgnval2  32795  pmtrcnel  33152  pmtrcnel2  33153  psgnfzto1stlem  33163  cycpmco2lem1  33189  cycpmco2  33196  cyc2fvx  33197  cyc3co2  33203  cycpmrn  33206  tocyccntz  33207  cyc3evpm  33213  cyc3genpmlem  33214  isarchiofld  33262  drngidlhash  33496  qsidomlem2  33515  ssdifidlprm  33520  mxidlnzr  33529  drng0mxidl  33538  drngmxidl  33539  qsdrng  33559  rsprprmprmidl  33584  deg1prod  33645  vietadeg1  33715  ply1annnr  33841  constrrtll  33869  constrrtlc1  33870  constrrtcclem  33872  constrrtcc  33873  constrfin  33884  constrelextdg2  33885  cos9thpiminplylem3  33922  1smat1  33942  submateqlem1  33945  ordtconnlem1  34062  esumrnmpt2  34206  cntnevol  34366  signstfveq0a  34714  repr0  34749  reprlt  34757  reprinfz1  34760  cusgredgex  35297  2cycl2d  35314  acycgr1v  35324  derangenlem  35346  subfacp1lem1  35354  subfacp1lem3  35357  subfacp1lem5  35359  fmlasucdisj  35574  dfrdg4  36126  ifscgr  36219  cgrxfr  36230  btwnconn1lem8  36269  btwnconn3  36278  segcon2  36280  broutsideof3  36301  outsideoftr  36304  outsideofeq  36305  outsideofeu  36306  lineunray  36322  lineelsb2  36323  linethru  36328  unbdqndv2lem2  36685  knoppndvlem1  36687  knoppndvlem2  36688  knoppndvlem7  36693  knoppndvlem14  36700  bj-bary1lem  37486  bj-bary1lem1  37487  bj-bary1  37488  finxpreclem2  37566  finxp1o  37568  finxpreclem6  37572  fin2solem  37778  poimirlem9  37801  poimirlem15  37807  poimirlem20  37812  poimirlem24  37816  poimirlem25  37817  poimirlem27  37819  itg2addnclem2  37844  ftc1cnnc  37864  heibor1lem  37981  maxidln0  38217  lshpnelb  39281  lsatssn0  39299  lsatcv0  39328  lsat0cv  39330  lsatexch1  39343  l1cvat  39352  atlen0  39607  cvlsupr2  39640  atcvrj2b  39729  2atlt  39736  atbtwn  39743  3noncolr2  39746  4noncolr3  39750  3dimlem3  39758  3dimlem3OLDN  39759  3dimlem4  39761  3dimlem4OLDN  39762  3dim2  39765  1cvratex  39770  1cvrat  39773  ps-1  39774  ps-2  39775  hlatexch4  39778  3atlem4  39783  3atlem6  39785  4atlem0ae  39891  4atlem0be  39892  dalemccnedd  39984  dalemrotps  39988  dalem21  39991  dalem23  39993  dalem27  39996  dalem41  40010  dalem44  40013  dalem54  40023  lnatexN  40076  lnjatN  40077  llnexchb2lem  40165  llnexchb2  40166  lhpn0  40301  lhpexle3lem  40308  lhpmatb  40328  4atexlemswapqr  40360  4atexlemc  40366  4atexlemnclw  40367  4atexlemcnd  40369  4atexlemex4  40370  4atexlemex6  40371  4atex  40373  trlat  40466  trlval4  40485  cdlemc5  40492  cdlemd4  40498  cdlemd7  40501  cdlemd9  40503  cdleme0e  40514  cdleme3b  40526  cdleme3c  40527  cdleme3e  40529  cdleme3h  40532  cdleme7aa  40539  cdleme7e  40544  cdleme7ga  40545  cdleme9  40550  cdleme11c  40558  cdleme11e  40560  cdleme11fN  40561  cdleme11h  40563  cdleme11j  40564  cdleme11k  40565  cdleme15b  40572  cdleme15c  40573  cdleme17c  40585  cdleme18b  40589  cdlemesner  40593  cdleme20zN  40598  cdleme19c  40602  cdleme19d  40603  cdleme19e  40604  cdleme20m  40620  cdleme21a  40622  cdleme21b  40623  cdleme21c  40624  cdleme22f2  40644  cdleme28b  40668  cdleme36a  40757  cdleme36m  40758  cdleme41sn4aw  40772  cdleme43bN  40787  cdleme43dN  40789  cdleme46f2g2  40790  cdleme46f2g1  40791  cdleme4gfv  40804  cdlemeg46nlpq  40814  cdlemeg46req  40826  cdlemeg46fgN  40831  cdlemf1  40858  cdlemg8b  40925  cdlemg9a  40929  cdlemg12g  40946  cdlemg12  40947  cdlemg13a  40948  cdlemg17pq  40969  cdlemg18a  40975  cdlemg18c  40977  cdlemg19a  40980  cdlemg19  40981  cdlemg21  40983  cdlemg31b0N  40991  cdlemg31b0a  40992  cdlemg31c  40996  cdlemg33b0  40998  cdlemg33c0  40999  trlcone  41025  cdlemg42  41026  cdlemg44a  41028  cdlemg46  41032  cdlemh1  41112  cdlemh2  41113  cdlemh  41114  cdlemj3  41120  cdlemk3  41130  cdlemki  41138  cdlemksv2  41144  cdlemk12  41147  cdlemk14  41151  cdlemk15  41152  cdlemk7u  41167  cdlemk11u  41168  cdlemk12u  41169  cdlemk21N  41170  cdlemk20  41171  cdlemk22  41190  cdlemk26-3  41203  cdlemk27-3  41204  cdlemk28-3  41205  cdlemkfid3N  41222  cdlemk11ta  41226  cdlemk47  41246  cdlemk54  41255  dia2dimlem1  41361  dochsat  41680  dochshpncl  41681  lclkrlem2b  41805  lcfrlem21  41860  baerlem5amN  42013  baerlem5bmN  42014  baerlem5abmN  42015  mapdindp4  42020  mapdheq2  42026  mapdheq2biN  42027  mapdh6aN  42032  mapdh6dN  42036  mapdh6eN  42037  mapdh6hN  42040  mapdh7eN  42045  mapdh7dN  42047  mapdh7fN  42048  mapdh8ab  42074  mapdh8ad  42076  mapdh8e  42081  mapdh9a  42086  mapdh9aOLDN  42087  hdmap1l6a  42106  hdmap1l6d  42110  hdmap1l6e  42111  hdmap1l6h  42114  hdmap1eulem  42119  hdmap1eulemOLDN  42120  hdmapval0  42130  hdmapeveclem  42131  hdmapval3lemN  42134  hdmap10lem  42136  hdmap11lem1  42138  hdmaprnlem3N  42147  hdmaprnlem9N  42154  hdmaprnlem3eN  42155  fzne2d  42271  lcmineqlem11  42330  3lexlogpow5ineq1  42345  3lexlogpow5ineq2  42346  3lexlogpow5ineq4  42347  3lexlogpow5ineq3  42348  3lexlogpow2ineq1  42349  3lexlogpow2ineq2  42350  3lexlogpow5ineq5  42351  aks4d1lem1  42353  dvrelog2b  42357  dvrelogpow2b  42359  aks4d1p1p3  42360  aks4d1p1p2  42361  aks4d1p1p4  42362  aks4d1p1p6  42364  aks4d1p1p7  42365  aks4d1p1p5  42366  aks4d1p1  42367  aks4d1p2  42368  aks4d1p3  42369  aks4d1p5  42371  aks4d1p6  42372  aks4d1p7d1  42373  aks4d1p7  42374  aks4d1p8d3  42377  aks4d1p8  42378  aks4d1p9  42379  fldhmf1  42381  aks6d1c2p2  42410  hashscontpow  42413  aks6d1c3  42414  aks6d1c5lem2  42429  2np3bcnp1  42435  2ap1caineq  42436  sticksstones1  42437  sticksstones2  42438  sticksstones10  42446  sticksstones12a  42448  sticksstones12  42449  sticksstones22  42459  aks6d1c6lem4  42464  aks6d1c7lem2  42472  unitscyglem2  42487  unitscyglem4  42489  aks5lem8  42492  xppss12  42522  mhpind  42873  jm2.26lem3  43279  rpnnen3lem  43309  rpnnen3  43310  imo72b2lem2  44444  imo72b2  44449  mnuprdlem1  44549  bcc0  44617  chordthmALT  45209  fnchoice  45310  refsum2cnlem1  45318  xrleneltd  45604  xrltned  45638  infleinf  45652  reclt0  45671  icoiccdif  45806  ressiooinf  45839  limcresiooub  45922  limcleqr  45924  limclner  45931  climxrre  46030  icccncfext  46167  cncfiooiccre  46175  dvnxpaek  46222  stoweidlem43  46323  stirlinglem5  46358  stirlinglem7  46360  dirkercncflem1  46383  fourierdlem24  46411  fourierdlem32  46419  fourierdlem33  46420  fourierdlem34  46421  fourierdlem35  46422  fourierdlem46  46432  fourierdlem48  46434  fourierdlem49  46435  fourierdlem64  46450  fourierdlem65  46451  fourierdlem74  46460  fourierdlem76  46462  fourierdlem79  46465  fourierdlem81  46467  fourierdlem91  46477  fourierdlem102  46488  fourierdlem114  46500  etransclem15  46529  etransclem24  46538  sge0rpcpnf  46701  sge0isum  46707  pimrecltpos  46988  m1modne  47630  minusmod5ne  47631  m1modnep2mod  47634  modmknepk  47644  modm2nep1  47648  modm1nep2  47650  setsnidel  47659  odz2prm2pw  47845  fmtnoprmfac1lem  47846  fmtnoprmfac1  47847  fmtnoprmfac2  47849  lighneallem1  47887  lighneallem3  47889  perfectALTVlem2  48004  usgrgrtrirex  48232  isubgr3stgrlem6  48253  gpgusgralem  48338  gpg3nbgrvtx0  48358  pgnioedg1  48390  pgnioedg2  48391  pgnioedg5  48394  nnsgrpnmnd  48460  lvecpsslmod  48789  affinecomb1  48984  affinecomb2  48985  1subrec1sub  48987  rrx2plord2  49004  line  49014  rrxline  49016  eenglngeehlnmlem2  49020  rrx2vlinest  49023  line2xlem  49035  2itscp  49063