Theorem necomd 2980

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

Syntax hints:   → wi 4   ≠ wne 2925

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 2701

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

This theorem is referenced by:  difsnb  4770  0nelop  5456  xpdifid  6141  f1ounsn  7247  resf1extb  7910  difsnen  9023  fofinf1o  9283  en2eleq  9961  en2other2  9962  ackbij1lem15  10186  infpssrlem5  10260  fin23lem24  10275  fin23lem31  10296  isf32lem9  10314  canthnumlem  10601  canthp1lem2  10606  npomex  10949  ltned  11310  lt0ne0  11644  recgt0  12028  zneo  12617  xrltne  13123  supxrbnd  13288  flltnz  13773  seqf1olem1  14006  nn0opthi  14235  hashtpg  14450  hash7g  14451  hashge3el3dif  14452  cats1un  14686  sumtp  15715  geoserg  15832  geolim  15836  geolim2  15837  tanadd  16135  ruclem6  16203  ruclem7  16204  isprm2lem  16651  isprm5  16677  oddprm  16781  pcmpt  16863  cshwshashlem3  17068  resshom  17381  ressco  17382  mrissmrcd  17601  rescco  17794  estrres  18100  smndex2dnrinv  18842  pmtrprfv  19383  symggen  19400  dprdcntz  19940  dprdres  19960  ablfac1b  20002  01eq0ringOLD  20440  nrhmzr  20446  lbspss  20989  lspsnnecom  21029  lspindp2l  21044  lspindp2  21045  islbs3  21065  lbsextlem4  21071  lidlnz  21152  uvcf1  21701  frlmup2  21708  psrridm  21872  coe1tmfv2  22161  coe1tmmul  22163  dmatmul  22384  mdetralt  22495  mdetunilem2  22500  mdetunilem6  22504  mdetunilem7  22505  maducoeval2  22527  madurid  22531  fvmptnn04ifa  22737  en2top  22872  cmpfi  23295  snfil  23751  tsmsfbas  24015  zcld  24702  iccpnfhmeo  24843  xrhmeo  24844  evth  24858  minveclem3b  25328  i1fres  25606  dvcnvlem  25880  ig1peu  26080  ig1pdvds  26085  aaliou3lem9  26258  taylthlem2  26282  taylthlem2OLD  26283  abelthlem2  26342  abelthlem7  26348  cos02pilt1  26435  tanregt0  26448  logcj  26515  argimgt0  26521  dvloglem  26557  logf1o2  26559  logbrec  26692  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  ang180lem4  26722  ang180lem5  26723  ang180  26724  isosctrlem3  26730  ssscongptld  26732  affineequivne  26737  angpieqvdlem  26738  angpieqvdlem2  26739  angpieqvd  26741  chordthmlem  26742  chordthmlem2  26743  chordthm  26747  asinneg  26796  ppiltx  27087  perfectlem2  27141  lgsneg  27232  lgsqr  27262  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem3  27293  lgsquad2  27297  2lgsoddprm  27327  dchrisum0flblem1  27419  noseponlem  27576  nosep1o  27593  nosep2o  27594  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  slerec  27731  0elright  27823  tgbtwnouttr  28424  tgifscgr  28435  tgcgrxfr  28445  tglngval  28478  tgfscgr  28495  tgbtwnconn1lem3  28501  tgbtwnconn3  28504  legtrid  28518  hltr  28537  hlbtwn  28538  btwnhl1  28539  btwnhl  28541  hlcgrex  28543  hlcgreulem  28544  lncom  28549  tgisline  28554  tglineeltr  28558  tglineelsb2  28559  tglinecom  28562  tglinethru  28563  ncolncol  28573  coltr  28574  coltr3  28575  symquadlem  28616  midexlem  28619  ragcol  28626  ragcgr  28634  perpneq  28641  footexALT  28645  footexlem1  28646  footexlem2  28647  foot  28649  footne  28650  colperpexlem3  28659  mideulem2  28661  opphllem  28662  midex  28664  opphllem1  28674  opphllem2  28675  opphllem3  28676  opphllem4  28677  opphllem5  28678  opphllem6  28679  outpasch  28682  hlpasch  28683  lnopp2hpgb  28690  colhp  28697  lmieu  28711  hypcgrlem1  28726  hypcgrlem2  28727  lnperpex  28730  trgcopy  28731  trgcopyeulem  28732  iscgra1  28737  cgrane2  28740  cgrane3  28741  cgrane4  28742  cgracgr  28745  cgraid  28746  cgraswap  28747  cgrcgra  28748  cgracom  28749  cgratr  28750  flatcgra  28751  cgraswaplr  28752  cgracol  28755  dfcgra2  28757  sacgr  28758  oacgr  28759  acopy  28760  acopyeu  28761  leagne2  28777  leagne3  28778  cgrg3col4  28780  tgsas1  28781  tgsas2  28783  tgasa1  28785  ttgcontlem1  28812  brbtwn2  28832  axlowdimlem15  28883  axlowdimlem16  28884  axcontlem8  28898  upgrex  29019  edglnl  29070  umgrvad2edg  29140  nbupgr  29271  nbumgrvtx  29273  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nbupgrres  29291  cplgr3v  29362  cusgrexilem2  29369  usgredgsscusgredg  29387  1hegrvtxdg1r  29436  1egrvtxdg1r  29438  1egrvtxdg0  29439  pthdadjvtx  29658  pthdlem2lem  29697  wspniunwspnon  29853  umgr2cwwk2dif  29993  3pthdlem1  30093  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  frgr3v  30204  1to3vfriswmgr  30209  frgrwopreglem5a  30240  frgrwopreglem3  30243  frgrhash2wsp  30261  staddi  32175  unidifsnne  32465  ifnefals  32477  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  33285  orngrmullt  33286  orngmullt  33287  ofldlt1  33291  ofldchr  33292  isarchiofld  33295  drngidlhash  33405  qsidomlem2  33424  ssdifidlprm  33429  mxidlnzr  33438  drng0mxidl  33447  drngmxidl  33448  qsdrng  33468  rsprprmprmidl  33493  ply1annnr  33693  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  constrfin  33736  constrelextdg2  33737  cos9thpiminplylem3  33774  1smat1  33794  submateqlem1  33797  ordtconnlem1  33914  esumrnmpt2  34058  cntnevol  34218  signstfveq0a  34567  repr0  34602  reprlt  34610  reprinfz1  34613  cusgredgex  35109  2cycl2d  35126  acycgr1v  35136  derangenlem  35158  subfacp1lem1  35166  subfacp1lem3  35169  subfacp1lem5  35171  fmlasucdisj  35386  dfrdg4  35939  ifscgr  36032  cgrxfr  36043  btwnconn1lem8  36082  btwnconn3  36091  segcon2  36093  broutsideof3  36114  outsideoftr  36117  outsideofeq  36118  outsideofeu  36119  lineunray  36135  lineelsb2  36136  linethru  36141  unbdqndv2lem2  36498  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem14  36513  bj-bary1lem  37298  bj-bary1lem1  37299  bj-bary1  37300  finxpreclem2  37378  finxp1o  37380  finxpreclem6  37384  fin2solem  37600  poimirlem9  37623  poimirlem15  37629  poimirlem20  37634  poimirlem24  37638  poimirlem25  37639  poimirlem27  37641  itg2addnclem2  37666  ftc1cnnc  37686  heibor1lem  37803  maxidln0  38039  lshpnelb  38977  lsatssn0  38995  lsatcv0  39024  lsat0cv  39026  lsatexch1  39039  l1cvat  39048  atlen0  39303  cvlsupr2  39336  atcvrj2b  39426  2atlt  39433  atbtwn  39440  3noncolr2  39443  4noncolr3  39447  3dimlem3  39455  3dimlem3OLDN  39456  3dimlem4  39458  3dimlem4OLDN  39459  3dim2  39462  1cvratex  39467  1cvrat  39470  ps-1  39471  ps-2  39472  hlatexch4  39475  3atlem4  39480  3atlem6  39482  4atlem0ae  39588  4atlem0be  39589  dalemccnedd  39681  dalemrotps  39685  dalem21  39688  dalem23  39690  dalem27  39693  dalem41  39707  dalem44  39710  dalem54  39720  lnatexN  39773  lnjatN  39774  llnexchb2lem  39862  llnexchb2  39863  lhpn0  39998  lhpexle3lem  40005  lhpmatb  40025  4atexlemswapqr  40057  4atexlemc  40063  4atexlemnclw  40064  4atexlemcnd  40066  4atexlemex4  40067  4atexlemex6  40068  4atex  40070  trlat  40163  trlval4  40182  cdlemc5  40189  cdlemd4  40195  cdlemd7  40198  cdlemd9  40200  cdleme0e  40211  cdleme3b  40223  cdleme3c  40224  cdleme3e  40226  cdleme3h  40229  cdleme7aa  40236  cdleme7e  40241  cdleme7ga  40242  cdleme9  40247  cdleme11c  40255  cdleme11e  40257  cdleme11fN  40258  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme15b  40269  cdleme15c  40270  cdleme17c  40282  cdleme18b  40286  cdlemesner  40290  cdleme20zN  40295  cdleme19c  40299  cdleme19d  40300  cdleme19e  40301  cdleme20m  40317  cdleme21a  40319  cdleme21b  40320  cdleme21c  40321  cdleme22f2  40341  cdleme28b  40365  cdleme36a  40454  cdleme36m  40455  cdleme41sn4aw  40469  cdleme43bN  40484  cdleme43dN  40486  cdleme46f2g2  40487  cdleme46f2g1  40488  cdleme4gfv  40501  cdlemeg46nlpq  40511  cdlemeg46req  40523  cdlemeg46fgN  40528  cdlemf1  40555  cdlemg8b  40622  cdlemg9a  40626  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg17pq  40666  cdlemg18a  40672  cdlemg18c  40674  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg31b0N  40688  cdlemg31b0a  40689  cdlemg31c  40693  cdlemg33b0  40695  cdlemg33c0  40696  trlcone  40722  cdlemg42  40723  cdlemg44a  40725  cdlemg46  40729  cdlemh1  40809  cdlemh2  40810  cdlemh  40811  cdlemj3  40817  cdlemk3  40827  cdlemki  40835  cdlemksv2  40841  cdlemk12  40844  cdlemk14  40848  cdlemk15  40849  cdlemk7u  40864  cdlemk11u  40865  cdlemk12u  40866  cdlemk21N  40867  cdlemk20  40868  cdlemk22  40887  cdlemk26-3  40900  cdlemk27-3  40901  cdlemk28-3  40902  cdlemkfid3N  40919  cdlemk11ta  40923  cdlemk47  40943  cdlemk54  40952  dia2dimlem1  41058  dochsat  41377  dochshpncl  41378  lclkrlem2b  41502  lcfrlem21  41557  baerlem5amN  41710  baerlem5bmN  41711  baerlem5abmN  41712  mapdindp4  41717  mapdheq2  41723  mapdheq2biN  41724  mapdh6aN  41729  mapdh6dN  41733  mapdh6eN  41734  mapdh6hN  41737  mapdh7eN  41742  mapdh7dN  41744  mapdh7fN  41745  mapdh8ab  41771  mapdh8ad  41773  mapdh8e  41778  mapdh9a  41783  mapdh9aOLDN  41784  hdmap1l6a  41803  hdmap1l6d  41807  hdmap1l6e  41808  hdmap1l6h  41811  hdmap1eulem  41816  hdmap1eulemOLDN  41817  hdmapval0  41827  hdmapeveclem  41828  hdmapval3lemN  41831  hdmap10lem  41833  hdmap11lem1  41835  hdmaprnlem3N  41844  hdmaprnlem9N  41851  hdmaprnlem3eN  41852  fzne2d  41968  lcmineqlem11  42027  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  fldhmf1  42078  aks6d1c2p2  42107  hashscontpow  42110  aks6d1c3  42111  aks6d1c5lem2  42126  2np3bcnp1  42132  2ap1caineq  42133  sticksstones1  42134  sticksstones2  42135  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem4  42161  aks6d1c7lem2  42169  unitscyglem2  42184  unitscyglem4  42186  aks5lem8  42189  xppss12  42217  mhpind  42582  jm2.26lem3  42990  rpnnen3lem  43020  rpnnen3  43021  imo72b2lem2  44156  imo72b2  44161  mnuprdlem1  44261  bcc0  44329  chordthmALT  44922  fnchoice  45023  refsum2cnlem1  45031  xrleneltd  45319  xrltned  45353  infleinf  45368  reclt0  45387  icoiccdif  45522  ressiooinf  45555  limcresiooub  45640  limcleqr  45642  limclner  45649  climxrre  45748  icccncfext  45885  cncfiooiccre  45893  dvnxpaek  45940  stoweidlem43  46041  stirlinglem5  46076  stirlinglem7  46078  dirkercncflem1  46101  fourierdlem24  46129  fourierdlem32  46137  fourierdlem33  46138  fourierdlem34  46139  fourierdlem35  46140  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem91  46195  fourierdlem102  46206  fourierdlem114  46218  etransclem15  46247  etransclem24  46256  sge0rpcpnf  46419  sge0isum  46425  pimrecltpos  46706  pimiooltgt  46708  m1modne  47349  minusmod5ne  47350  m1modnep2mod  47353  modmknepk  47363  modm2nep1  47367  modm1nep2  47369  setsnidel  47378  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  fmtnoprmfac2  47568  lighneallem1  47606  lighneallem3  47608  perfectALTVlem2  47723  usgrgrtrirex  47949  isubgr3stgrlem6  47970  gpgusgralem  48047  gpg3nbgrvtx0  48067  pgnioedg1  48098  pgnioedg2  48099  pgnioedg5  48102  nnsgrpnmnd  48166  lvecpsslmod  48496  affinecomb1  48691  affinecomb2  48692  1subrec1sub  48694  rrx2plord2  48711  line  48721  rrxline  48723  eenglngeehlnmlem2  48727  rrx2vlinest  48730  line2xlem  48742  2itscp  48770