Theorem necomd 2999

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

Syntax hints:   → wi 4   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  difsnb  4739  0nelop  5410  xpdifid  6071  difsnen  8840  fofinf1o  9094  en2eleq  9764  en2other2  9765  ackbij1lem15  9990  infpssrlem5  10063  fin23lem24  10078  fin23lem31  10099  isf32lem9  10117  canthnumlem  10404  canthp1lem2  10409  npomex  10752  ltned  11111  lt0ne0  11441  recgt0  11821  zneo  12403  xrltne  12897  supxrbnd  13062  flltnz  13531  seqf1olem1  13762  nn0opthi  13984  hashtpg  14199  hashge3el3dif  14200  cats1un  14434  sumtp  15461  geoserg  15578  geolim  15582  geolim2  15583  tanadd  15876  ruclem6  15944  ruclem7  15945  isprm2lem  16386  isprm5  16412  oddprm  16511  pcmpt  16593  cshwshashlem3  16799  resshom  17129  ressco  17130  mrissmrcd  17349  rescco  17545  estrres  17856  smndex2dnrinv  18554  pmtrprfv  19061  symggen  19078  dprdcntz  19611  dprdres  19631  ablfac1b  19673  lbspss  20344  lspsnnecom  20381  lspindp2l  20396  lspindp2  20397  islbs3  20417  lbsextlem4  20423  sralemOLD  20440  lidlnz  20499  01eq0ring  20543  uvcf1  20999  frlmup2  21006  psrridm  21173  coe1tmfv2  21446  coe1tmmul  21448  dmatmul  21646  mdetralt  21757  mdetunilem2  21762  mdetunilem6  21766  mdetunilem7  21767  maducoeval2  21789  madurid  21793  fvmptnn04ifa  21999  en2top  22135  cmpfi  22559  snfil  23015  tsmsfbas  23279  zcld  23976  iccpnfhmeo  24108  xrhmeo  24109  evth  24122  minveclem3b  24592  i1fres  24870  dvcnvlem  25140  ig1peu  25336  ig1pdvds  25341  aaliou3lem9  25510  taylthlem2  25533  abelthlem2  25591  abelthlem7  25597  cos02pilt1  25682  tanregt0  25695  logcj  25761  argimgt0  25767  dvloglem  25803  logf1o2  25805  logbrec  25932  ang180lem1  25959  ang180lem2  25960  ang180lem3  25961  ang180lem4  25962  ang180lem5  25963  ang180  25964  isosctrlem3  25970  ssscongptld  25972  affineequivne  25977  angpieqvdlem  25978  angpieqvdlem2  25979  angpieqvd  25981  chordthmlem  25982  chordthmlem2  25983  chordthm  25987  asinneg  26036  ppiltx  26326  perfectlem2  26378  lgsneg  26469  lgsqr  26499  lgseisenlem4  26526  lgsquadlem1  26528  lgsquadlem3  26530  lgsquad2  26534  2lgsoddprm  26564  dchrisum0flblem1  26656  tgbtwnouttr  26858  tgifscgr  26869  tgcgrxfr  26879  tglngval  26912  tgfscgr  26929  tgbtwnconn1lem3  26935  tgbtwnconn3  26938  legtrid  26952  hltr  26971  hlbtwn  26972  btwnhl1  26973  btwnhl  26975  hlcgrex  26977  hlcgreulem  26978  lncom  26983  tgisline  26988  tglineeltr  26992  tglineelsb2  26993  tglinecom  26996  tglinethru  26997  ncolncol  27007  coltr  27008  coltr3  27009  symquadlem  27050  midexlem  27053  ragcol  27060  ragcgr  27068  perpneq  27075  footexALT  27079  footexlem1  27080  footexlem2  27081  foot  27083  footne  27084  colperpexlem3  27093  mideulem2  27095  opphllem  27096  midex  27098  opphllem1  27108  opphllem2  27109  opphllem3  27110  opphllem4  27111  opphllem5  27112  opphllem6  27113  outpasch  27116  hlpasch  27117  lnopp2hpgb  27124  colhp  27131  lmieu  27145  hypcgrlem1  27160  hypcgrlem2  27161  lnperpex  27164  trgcopy  27165  trgcopyeulem  27166  iscgra1  27171  cgrane2  27174  cgrane3  27175  cgrane4  27176  cgracgr  27179  cgraid  27180  cgraswap  27181  cgrcgra  27182  cgracom  27183  cgratr  27184  flatcgra  27185  cgraswaplr  27186  cgracol  27189  dfcgra2  27191  sacgr  27192  oacgr  27193  acopy  27194  acopyeu  27195  leagne2  27211  leagne3  27212  cgrg3col4  27214  tgsas1  27215  tgsas2  27217  tgasa1  27219  ttgcontlem1  27252  cchhllemOLD  27255  brbtwn2  27273  axlowdimlem15  27324  axlowdimlem16  27325  axcontlem8  27339  upgrex  27462  edglnl  27513  umgrvad2edg  27580  nbupgr  27711  nbumgrvtx  27713  nbgr2vtx1edg  27717  nbuhgr2vtx1edgb  27719  nbupgrres  27731  cplgr3v  27802  cusgrexilem2  27809  usgredgsscusgredg  27826  1hegrvtxdg1r  27875  1egrvtxdg1r  27877  1egrvtxdg0  27878  pthdadjvtx  28098  pthdlem2lem  28135  wspniunwspnon  28288  umgr2cwwk2dif  28428  3pthdlem1  28528  uhgr3cyclex  28546  upgr4cycl4dv4e  28549  frgr3v  28639  1to3vfriswmgr  28644  frgrwopreglem5a  28675  frgrwopreglem3  28678  frgrhash2wsp  28696  staddi  30608  unidifsnne  30884  coprprop  31032  pmtrcnel  31358  pmtrcnel2  31359  psgnfzto1stlem  31367  cycpmco2lem1  31393  cycpmco2  31400  cyc2fvx  31401  cyc3co2  31407  cycpmrn  31410  tocyccntz  31411  cyc3evpm  31417  cyc3genpmlem  31418  ornglmullt  31506  orngrmullt  31507  orngmullt  31508  ofldlt1  31512  ofldchr  31513  isarchiofld  31516  qsidomlem2  31629  mxidlnzr  31639  1smat1  31754  submateqlem1  31757  madjusmdetlem2  31778  ordtconnlem1  31874  esumrnmpt2  32036  cntnevol  32196  signstfveq0a  32555  repr0  32591  reprlt  32599  reprinfz1  32602  cusgredgex  33083  2cycl2d  33101  acycgr1v  33111  derangenlem  33133  subfacp1lem1  33141  subfacp1lem3  33144  subfacp1lem5  33146  fmlasucdisj  33361  noseponlem  33867  nosep1o  33884  nosep2o  33885  nosupbnd2lem1  33918  noinfbnd2lem1  33933  noetasuplem4  33939  noetainflem4  33943  slerec  34013  dfrdg4  34253  ifscgr  34346  cgrxfr  34357  btwnconn1lem8  34396  btwnconn3  34405  segcon2  34407  broutsideof3  34428  outsideoftr  34431  outsideofeq  34432  outsideofeu  34433  lineunray  34449  lineelsb2  34450  linethru  34455  unbdqndv2lem2  34690  knoppndvlem1  34692  knoppndvlem2  34693  knoppndvlem7  34698  knoppndvlem14  34705  bj-bary1lem  35481  bj-bary1lem1  35482  bj-bary1  35483  finxpreclem2  35561  finxp1o  35563  finxpreclem6  35567  fin2solem  35763  poimirlem9  35786  poimirlem15  35792  poimirlem20  35797  poimirlem24  35801  poimirlem25  35802  poimirlem27  35804  itg2addnclem2  35829  ftc1cnnc  35849  heibor1lem  35967  maxidln0  36203  lshpnelb  36998  lsatssn0  37016  lsatcv0  37045  lsat0cv  37047  lsatexch1  37060  l1cvat  37069  atlen0  37324  cvlsupr2  37357  atcvrj2b  37446  2atlt  37453  atbtwn  37460  3noncolr2  37463  4noncolr3  37467  3dimlem3  37475  3dimlem3OLDN  37476  3dimlem4  37478  3dimlem4OLDN  37479  3dim2  37482  1cvratex  37487  1cvrat  37490  ps-1  37491  ps-2  37492  hlatexch4  37495  3atlem4  37500  3atlem6  37502  4atlem0ae  37608  4atlem0be  37609  dalemccnedd  37701  dalemrotps  37705  dalem21  37708  dalem23  37710  dalem27  37713  dalem41  37727  dalem44  37730  dalem54  37740  lnatexN  37793  lnjatN  37794  llnexchb2lem  37882  llnexchb2  37883  lhpn0  38018  lhpexle3lem  38025  lhpmatb  38045  4atexlemswapqr  38077  4atexlemc  38083  4atexlemnclw  38084  4atexlemcnd  38086  4atexlemex4  38087  4atexlemex6  38088  4atex  38090  trlat  38183  trlval4  38202  cdlemc5  38209  cdlemd4  38215  cdlemd7  38218  cdlemd9  38220  cdleme0e  38231  cdleme3b  38243  cdleme3c  38244  cdleme3e  38246  cdleme3h  38249  cdleme7aa  38256  cdleme7e  38261  cdleme7ga  38262  cdleme9  38267  cdleme11c  38275  cdleme11e  38277  cdleme11fN  38278  cdleme11h  38280  cdleme11j  38281  cdleme11k  38282  cdleme15b  38289  cdleme15c  38290  cdleme17c  38302  cdleme18b  38306  cdlemesner  38310  cdleme20zN  38315  cdleme19c  38319  cdleme19d  38320  cdleme19e  38321  cdleme20m  38337  cdleme21a  38339  cdleme21b  38340  cdleme21c  38341  cdleme22f2  38361  cdleme28b  38385  cdleme36a  38474  cdleme36m  38475  cdleme41sn4aw  38489  cdleme43bN  38504  cdleme43dN  38506  cdleme46f2g2  38507  cdleme46f2g1  38508  cdleme4gfv  38521  cdlemeg46nlpq  38531  cdlemeg46req  38543  cdlemeg46fgN  38548  cdlemf1  38575  cdlemg8b  38642  cdlemg9a  38646  cdlemg12g  38663  cdlemg12  38664  cdlemg13a  38665  cdlemg17pq  38686  cdlemg18a  38692  cdlemg18c  38694  cdlemg19a  38697  cdlemg19  38698  cdlemg21  38700  cdlemg31b0N  38708  cdlemg31b0a  38709  cdlemg31c  38713  cdlemg33b0  38715  cdlemg33c0  38716  trlcone  38742  cdlemg42  38743  cdlemg44a  38745  cdlemg46  38749  cdlemh1  38829  cdlemh2  38830  cdlemh  38831  cdlemj3  38837  cdlemk3  38847  cdlemki  38855  cdlemksv2  38861  cdlemk12  38864  cdlemk14  38868  cdlemk15  38869  cdlemk7u  38884  cdlemk11u  38885  cdlemk12u  38886  cdlemk21N  38887  cdlemk20  38888  cdlemk22  38907  cdlemk26-3  38920  cdlemk27-3  38921  cdlemk28-3  38922  cdlemkfid3N  38939  cdlemk11ta  38943  cdlemk47  38963  cdlemk54  38972  dia2dimlem1  39078  dochsat  39397  dochshpncl  39398  lclkrlem2b  39522  lcfrlem21  39577  baerlem5amN  39730  baerlem5bmN  39731  baerlem5abmN  39732  mapdindp4  39737  mapdheq2  39743  mapdheq2biN  39744  mapdh6aN  39749  mapdh6dN  39753  mapdh6eN  39754  mapdh6hN  39757  mapdh7eN  39762  mapdh7dN  39764  mapdh7fN  39765  mapdh8ab  39791  mapdh8ad  39793  mapdh8e  39798  mapdh9a  39803  mapdh9aOLDN  39804  hdmap1l6a  39823  hdmap1l6d  39827  hdmap1l6e  39828  hdmap1l6h  39831  hdmap1eulem  39836  hdmap1eulemOLDN  39837  hdmapval0  39847  hdmapeveclem  39848  hdmapval3lemN  39851  hdmap10lem  39853  hdmap11lem1  39855  hdmaprnlem3N  39864  hdmaprnlem9N  39871  hdmaprnlem3eN  39872  fzne2d  39989  lcmineqlem11  40047  3lexlogpow5ineq1  40062  3lexlogpow5ineq2  40063  3lexlogpow5ineq4  40064  3lexlogpow5ineq3  40065  3lexlogpow2ineq1  40066  3lexlogpow2ineq2  40067  3lexlogpow5ineq5  40068  aks4d1lem1  40070  dvrelog2b  40074  dvrelogpow2b  40076  aks4d1p1p3  40077  aks4d1p1p2  40078  aks4d1p1p4  40079  aks4d1p1p6  40081  aks4d1p1p7  40082  aks4d1p1p5  40083  aks4d1p1  40084  aks4d1p2  40085  aks4d1p3  40086  aks4d1p5  40088  aks4d1p6  40089  aks4d1p7d1  40090  aks4d1p7  40091  aks4d1p8d3  40094  aks4d1p8  40095  aks4d1p9  40096  2np3bcnp1  40100  2ap1caineq  40101  sticksstones1  40102  sticksstones2  40103  sticksstones10  40111  sticksstones12a  40113  sticksstones12  40114  sticksstones22  40124  metakunt7  40131  metakunt12  40136  metakunt22  40146  xppss12  40204  mhpind  40283  jm2.26lem3  40823  rpnnen3lem  40853  rpnnen3  40854  imo72b2lem0  41776  imo72b2lem2  41778  imo72b2  41783  mnuprdlem1  41890  bcc0  41958  chordthmALT  42553  fnchoice  42572  refsum2cnlem1  42580  xrleneltd  42862  xrltned  42896  infleinf  42911  reclt0  42931  icoiccdif  43062  ressiooinf  43095  limcresiooub  43183  limcleqr  43185  limclner  43192  climxrre  43291  icccncfext  43428  cncfiooiccre  43436  dvnxpaek  43483  stoweidlem43  43584  stirlinglem5  43619  stirlinglem7  43621  dirkercncflem1  43644  fourierdlem24  43672  fourierdlem32  43680  fourierdlem33  43681  fourierdlem34  43682  fourierdlem35  43683  fourierdlem46  43693  fourierdlem48  43695  fourierdlem49  43696  fourierdlem64  43711  fourierdlem65  43712  fourierdlem74  43721  fourierdlem76  43723  fourierdlem79  43726  fourierdlem81  43728  fourierdlem91  43738  fourierdlem102  43749  fourierdlem114  43761  etransclem15  43790  etransclem24  43799  sge0rpcpnf  43959  sge0isum  43965  pimrecltpos  44245  pimiooltgt  44247  setsnidel  44829  odz2prm2pw  45015  fmtnoprmfac1lem  45016  fmtnoprmfac1  45017  fmtnoprmfac2  45019  lighneallem1  45057  lighneallem3  45059  perfectALTVlem2  45174  nnsgrpnmnd  45372  nrhmzr  45431  lvecpsslmod  45848  affinecomb1  46048  affinecomb2  46049  1subrec1sub  46051  rrx2plord2  46068  line  46078  rrxline  46080  eenglngeehlnmlem2  46084  rrx2vlinest  46087  line2xlem  46099  2itscp  46127