Theorem necomd 2993

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

Syntax hints:   → wi 4   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  difsnb  4810  0nelop  5505  xpdifid  6189  f1ounsn  7291  difsnen  9091  fofinf1o  9369  en2eleq  10045  en2other2  10046  ackbij1lem15  10270  infpssrlem5  10344  fin23lem24  10359  fin23lem31  10380  isf32lem9  10398  canthnumlem  10685  canthp1lem2  10690  npomex  11033  ltned  11394  lt0ne0  11726  recgt0  12110  zneo  12698  xrltne  13201  supxrbnd  13366  flltnz  13847  seqf1olem1  14078  nn0opthi  14305  hashtpg  14520  hash7g  14521  hashge3el3dif  14522  cats1un  14755  sumtp  15781  geoserg  15898  geolim  15902  geolim2  15903  tanadd  16199  ruclem6  16267  ruclem7  16268  isprm2lem  16714  isprm5  16740  oddprm  16843  pcmpt  16925  cshwshashlem3  17131  resshom  17464  ressco  17465  mrissmrcd  17684  rescco  17880  estrres  18194  smndex2dnrinv  18940  pmtrprfv  19485  symggen  19502  dprdcntz  20042  dprdres  20062  ablfac1b  20104  01eq0ringOLD  20547  nrhmzr  20553  lbspss  21098  lspsnnecom  21138  lspindp2l  21153  lspindp2  21154  islbs3  21174  lbsextlem4  21180  sralemOLD  21193  lidlnz  21269  uvcf1  21829  frlmup2  21836  psrridm  22000  coe1tmfv2  22293  coe1tmmul  22295  dmatmul  22518  mdetralt  22629  mdetunilem2  22634  mdetunilem6  22638  mdetunilem7  22639  maducoeval2  22661  madurid  22665  fvmptnn04ifa  22871  en2top  23007  cmpfi  23431  snfil  23887  tsmsfbas  24151  zcld  24848  iccpnfhmeo  24989  xrhmeo  24990  evth  25004  minveclem3b  25475  i1fres  25754  dvcnvlem  26028  ig1peu  26228  ig1pdvds  26233  aaliou3lem9  26406  taylthlem2  26430  taylthlem2OLD  26431  abelthlem2  26490  abelthlem7  26496  cos02pilt1  26582  tanregt0  26595  logcj  26662  argimgt0  26668  dvloglem  26704  logf1o2  26706  logbrec  26839  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  ang180lem4  26869  ang180lem5  26870  ang180  26871  isosctrlem3  26877  ssscongptld  26879  affineequivne  26884  angpieqvdlem  26885  angpieqvdlem2  26886  angpieqvd  26888  chordthmlem  26889  chordthmlem2  26890  chordthm  26894  asinneg  26943  ppiltx  27234  perfectlem2  27288  lgsneg  27379  lgsqr  27409  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem3  27440  lgsquad2  27444  2lgsoddprm  27474  dchrisum0flblem1  27566  noseponlem  27723  nosep1o  27740  nosep2o  27741  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  slerec  27878  0elright  27963  tgbtwnouttr  28519  tgifscgr  28530  tgcgrxfr  28540  tglngval  28573  tgfscgr  28590  tgbtwnconn1lem3  28596  tgbtwnconn3  28599  legtrid  28613  hltr  28632  hlbtwn  28633  btwnhl1  28634  btwnhl  28636  hlcgrex  28638  hlcgreulem  28639  lncom  28644  tgisline  28649  tglineeltr  28653  tglineelsb2  28654  tglinecom  28657  tglinethru  28658  ncolncol  28668  coltr  28669  coltr3  28670  symquadlem  28711  midexlem  28714  ragcol  28721  ragcgr  28729  perpneq  28736  footexALT  28740  footexlem1  28741  footexlem2  28742  foot  28744  footne  28745  colperpexlem3  28754  mideulem2  28756  opphllem  28757  midex  28759  opphllem1  28769  opphllem2  28770  opphllem3  28771  opphllem4  28772  opphllem5  28773  opphllem6  28774  outpasch  28777  hlpasch  28778  lnopp2hpgb  28785  colhp  28792  lmieu  28806  hypcgrlem1  28821  hypcgrlem2  28822  lnperpex  28825  trgcopy  28826  trgcopyeulem  28827  iscgra1  28832  cgrane2  28835  cgrane3  28836  cgrane4  28837  cgracgr  28840  cgraid  28841  cgraswap  28842  cgrcgra  28843  cgracom  28844  cgratr  28845  flatcgra  28846  cgraswaplr  28847  cgracol  28850  dfcgra2  28852  sacgr  28853  oacgr  28854  acopy  28855  acopyeu  28856  leagne2  28872  leagne3  28873  cgrg3col4  28875  tgsas1  28876  tgsas2  28878  tgasa1  28880  ttgcontlem1  28913  cchhllemOLD  28916  brbtwn2  28934  axlowdimlem15  28985  axlowdimlem16  28986  axcontlem8  29000  upgrex  29123  edglnl  29174  umgrvad2edg  29244  nbupgr  29375  nbumgrvtx  29377  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nbupgrres  29395  cplgr3v  29466  cusgrexilem2  29473  usgredgsscusgredg  29491  1hegrvtxdg1r  29540  1egrvtxdg1r  29542  1egrvtxdg0  29543  pthdadjvtx  29762  pthdlem2lem  29799  wspniunwspnon  29952  umgr2cwwk2dif  30092  3pthdlem1  30192  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  frgr3v  30303  1to3vfriswmgr  30308  frgrwopreglem5a  30339  frgrwopreglem3  30342  frgrhash2wsp  30360  staddi  32274  unidifsnne  32561  ifnefals  32568  coprprop  32713  pmtrcnel  33091  pmtrcnel2  33092  psgnfzto1stlem  33102  cycpmco2lem1  33128  cycpmco2  33135  cyc2fvx  33136  cyc3co2  33142  cycpmrn  33145  tocyccntz  33146  cyc3evpm  33152  cyc3genpmlem  33153  ornglmullt  33316  orngrmullt  33317  orngmullt  33318  ofldlt1  33322  ofldchr  33323  isarchiofld  33326  drngidlhash  33441  qsidomlem2  33460  ssdifidlprm  33465  mxidlnzr  33474  drng0mxidl  33483  drngmxidl  33484  qsdrng  33504  rsprprmprmidl  33529  ply1annnr  33710  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrfin  33750  constrelextdg2  33751  1smat1  33764  submateqlem1  33767  ordtconnlem1  33884  esumrnmpt2  34048  cntnevol  34208  signstfveq0a  34569  repr0  34604  reprlt  34612  reprinfz1  34615  cusgredgex  35105  2cycl2d  35123  acycgr1v  35133  derangenlem  35155  subfacp1lem1  35163  subfacp1lem3  35166  subfacp1lem5  35168  fmlasucdisj  35383  dfrdg4  35932  ifscgr  36025  cgrxfr  36036  btwnconn1lem8  36075  btwnconn3  36084  segcon2  36086  broutsideof3  36107  outsideoftr  36110  outsideofeq  36111  outsideofeu  36112  lineunray  36128  lineelsb2  36129  linethru  36134  unbdqndv2lem2  36492  knoppndvlem1  36494  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem14  36507  bj-bary1lem  37292  bj-bary1lem1  37293  bj-bary1  37294  finxpreclem2  37372  finxp1o  37374  finxpreclem6  37378  fin2solem  37592  poimirlem9  37615  poimirlem15  37621  poimirlem20  37626  poimirlem24  37630  poimirlem25  37631  poimirlem27  37633  itg2addnclem2  37658  ftc1cnnc  37678  heibor1lem  37795  maxidln0  38031  lshpnelb  38965  lsatssn0  38983  lsatcv0  39012  lsat0cv  39014  lsatexch1  39027  l1cvat  39036  atlen0  39291  cvlsupr2  39324  atcvrj2b  39414  2atlt  39421  atbtwn  39428  3noncolr2  39431  4noncolr3  39435  3dimlem3  39443  3dimlem3OLDN  39444  3dimlem4  39446  3dimlem4OLDN  39447  3dim2  39450  1cvratex  39455  1cvrat  39458  ps-1  39459  ps-2  39460  hlatexch4  39463  3atlem4  39468  3atlem6  39470  4atlem0ae  39576  4atlem0be  39577  dalemccnedd  39669  dalemrotps  39673  dalem21  39676  dalem23  39678  dalem27  39681  dalem41  39695  dalem44  39698  dalem54  39708  lnatexN  39761  lnjatN  39762  llnexchb2lem  39850  llnexchb2  39851  lhpn0  39986  lhpexle3lem  39993  lhpmatb  40013  4atexlemswapqr  40045  4atexlemc  40051  4atexlemnclw  40052  4atexlemcnd  40054  4atexlemex4  40055  4atexlemex6  40056  4atex  40058  trlat  40151  trlval4  40170  cdlemc5  40177  cdlemd4  40183  cdlemd7  40186  cdlemd9  40188  cdleme0e  40199  cdleme3b  40211  cdleme3c  40212  cdleme3e  40214  cdleme3h  40217  cdleme7aa  40224  cdleme7e  40229  cdleme7ga  40230  cdleme9  40235  cdleme11c  40243  cdleme11e  40245  cdleme11fN  40246  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme15b  40257  cdleme15c  40258  cdleme17c  40270  cdleme18b  40274  cdlemesner  40278  cdleme20zN  40283  cdleme19c  40287  cdleme19d  40288  cdleme19e  40289  cdleme20m  40305  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme22f2  40329  cdleme28b  40353  cdleme36a  40442  cdleme36m  40443  cdleme41sn4aw  40457  cdleme43bN  40472  cdleme43dN  40474  cdleme46f2g2  40475  cdleme46f2g1  40476  cdleme4gfv  40489  cdlemeg46nlpq  40499  cdlemeg46req  40511  cdlemeg46fgN  40516  cdlemf1  40543  cdlemg8b  40610  cdlemg9a  40614  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg17pq  40654  cdlemg18a  40660  cdlemg18c  40662  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg31b0N  40676  cdlemg31b0a  40677  cdlemg31c  40681  cdlemg33b0  40683  cdlemg33c0  40684  trlcone  40710  cdlemg42  40711  cdlemg44a  40713  cdlemg46  40717  cdlemh1  40797  cdlemh2  40798  cdlemh  40799  cdlemj3  40805  cdlemk3  40815  cdlemki  40823  cdlemksv2  40829  cdlemk12  40832  cdlemk14  40836  cdlemk15  40837  cdlemk7u  40852  cdlemk11u  40853  cdlemk12u  40854  cdlemk21N  40855  cdlemk20  40856  cdlemk22  40875  cdlemk26-3  40888  cdlemk27-3  40889  cdlemk28-3  40890  cdlemkfid3N  40907  cdlemk11ta  40911  cdlemk47  40931  cdlemk54  40940  dia2dimlem1  41046  dochsat  41365  dochshpncl  41366  lclkrlem2b  41490  lcfrlem21  41545  baerlem5amN  41698  baerlem5bmN  41699  baerlem5abmN  41700  mapdindp4  41705  mapdheq2  41711  mapdheq2biN  41712  mapdh6aN  41717  mapdh6dN  41721  mapdh6eN  41722  mapdh6hN  41725  mapdh7eN  41730  mapdh7dN  41732  mapdh7fN  41733  mapdh8ab  41759  mapdh8ad  41761  mapdh8e  41766  mapdh9a  41771  mapdh9aOLDN  41772  hdmap1l6a  41791  hdmap1l6d  41795  hdmap1l6e  41796  hdmap1l6h  41799  hdmap1eulem  41804  hdmap1eulemOLDN  41805  hdmapval0  41815  hdmapeveclem  41816  hdmapval3lemN  41819  hdmap10lem  41821  hdmap11lem1  41823  hdmaprnlem3N  41832  hdmaprnlem9N  41839  hdmaprnlem3eN  41840  fzne2d  41961  lcmineqlem11  42020  3lexlogpow5ineq1  42035  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d3  42067  aks4d1p8  42068  aks4d1p9  42069  fldhmf1  42071  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c3  42104  aks6d1c5lem2  42119  2np3bcnp1  42125  2ap1caineq  42126  sticksstones1  42127  sticksstones2  42128  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem4  42154  aks6d1c7lem2  42162  unitscyglem2  42177  unitscyglem4  42179  aks5lem8  42182  metakunt7  42192  metakunt12  42197  metakunt22  42207  xppss12  42246  mhpind  42580  jm2.26lem3  42989  rpnnen3lem  43019  rpnnen3  43020  imo72b2lem2  44156  imo72b2  44161  mnuprdlem1  44267  bcc0  44335  chordthmALT  44930  fnchoice  44966  refsum2cnlem1  44974  xrleneltd  45272  xrltned  45306  infleinf  45321  reclt0  45340  icoiccdif  45476  ressiooinf  45509  limcresiooub  45597  limcleqr  45599  limclner  45606  climxrre  45705  icccncfext  45842  cncfiooiccre  45850  dvnxpaek  45897  stoweidlem43  45998  stirlinglem5  46033  stirlinglem7  46035  dirkercncflem1  46058  fourierdlem24  46086  fourierdlem32  46094  fourierdlem33  46095  fourierdlem34  46096  fourierdlem35  46097  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem91  46152  fourierdlem102  46163  fourierdlem114  46175  etransclem15  46204  etransclem24  46213  sge0rpcpnf  46376  sge0isum  46382  pimrecltpos  46663  pimiooltgt  46665  m1modne  47287  minusmod5ne  47288  m1modnep2mod  47291  setsnidel  47301  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  fmtnoprmfac2  47491  lighneallem1  47529  lighneallem3  47531  perfectALTVlem2  47646  usgrgrtrirex  47852  isubgr3stgrlem6  47873  gpgusgralem  47945  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  nnsgrpnmnd  48021  lvecpsslmod  48352  affinecomb1  48551  affinecomb2  48552  1subrec1sub  48554  rrx2plord2  48571  line  48581  rrxline  48583  eenglngeehlnmlem2  48587  rrx2vlinest  48590  line2xlem  48602  2itscp  48630