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  7221  resf1extb  7879  difsnen  8992  fofinf1o  9237  en2eleq  9923  en2other2  9924  ackbij1lem15  10148  infpssrlem5  10222  fin23lem24  10237  fin23lem31  10258  isf32lem9  10276  canthnumlem  10564  canthp1lem2  10569  npomex  10912  ltned  11274  lt0ne0  11608  recgt0  11992  zneo  12580  xrltne  13082  supxrbnd  13248  flltnz  13736  seqf1olem1  13969  nn0opthi  14198  hashtpg  14413  hash7g  14414  hashge3el3dif  14415  cats1un  14649  sumtp  15677  geoserg  15794  geolim  15798  geolim2  15799  tanadd  16097  ruclem6  16165  ruclem7  16166  isprm2lem  16613  isprm5  16639  oddprm  16743  pcmpt  16825  cshwshashlem3  17030  resshom  17343  ressco  17344  mrissmrcd  17568  rescco  17761  estrres  18067  chnccat  18554  chnrev  18555  chnpof1  18558  smndex2dnrinv  18845  pmtrprfv  19387  symggen  19404  dprdcntz  19944  dprdres  19964  ablfac1b  20006  01eq0ringOLD  20469  nrhmzr  20475  ornglmullt  20807  orngrmullt  20808  orngmullt  20809  ofldlt1  20813  lbspss  21039  lspsnnecom  21079  lspindp2l  21094  lspindp2  21095  islbs3  21115  lbsextlem4  21121  lidlnz  21202  ofldchr  21536  uvcf1  21752  frlmup2  21759  psrridm  21923  coe1tmfv2  22222  coe1tmmul  22224  dmatmul  22446  mdetralt  22557  mdetunilem2  22562  mdetunilem6  22566  mdetunilem7  22567  maducoeval2  22589  madurid  22593  fvmptnn04ifa  22799  en2top  22934  cmpfi  23357  snfil  23813  tsmsfbas  24077  zcld  24763  iccpnfhmeo  24904  xrhmeo  24905  evth  24919  minveclem3b  25389  i1fres  25667  dvcnvlem  25941  ig1peu  26141  ig1pdvds  26146  aaliou3lem9  26319  taylthlem2  26343  taylthlem2OLD  26344  abelthlem2  26403  abelthlem7  26409  cos02pilt1  26496  tanregt0  26509  logcj  26576  argimgt0  26582  dvloglem  26618  logf1o2  26620  logbrec  26753  ang180lem1  26780  ang180lem2  26781  ang180lem3  26782  ang180lem4  26783  ang180lem5  26784  ang180  26785  isosctrlem3  26791  ssscongptld  26793  affineequivne  26798  angpieqvdlem  26799  angpieqvdlem2  26800  angpieqvd  26802  chordthmlem  26803  chordthmlem2  26804  chordthm  26808  asinneg  26857  ppiltx  27148  perfectlem2  27202  lgsneg  27293  lgsqr  27323  lgseisenlem4  27350  lgsquadlem1  27352  lgsquadlem3  27354  lgsquad2  27358  2lgsoddprm  27388  dchrisum0flblem1  27480  noseponlem  27637  nosep1o  27654  nosep2o  27655  nosupbnd2lem1  27688  noinfbnd2lem1  27703  noetasuplem4  27709  noetainflem4  27713  lesrec  27800  0elright  27913  tgbtwnouttr  28574  tgifscgr  28585  tgcgrxfr  28595  tglngval  28628  tgfscgr  28645  tgbtwnconn1lem3  28651  tgbtwnconn3  28654  legtrid  28668  hltr  28687  hlbtwn  28688  btwnhl1  28689  btwnhl  28691  hlcgrex  28693  hlcgreulem  28694  lncom  28699  tgisline  28704  tglineeltr  28708  tglineelsb2  28709  tglinecom  28712  tglinethru  28713  ncolncol  28723  coltr  28724  coltr3  28725  symquadlem  28766  midexlem  28769  ragcol  28776  ragcgr  28784  perpneq  28791  footexALT  28795  footexlem1  28796  footexlem2  28797  foot  28799  footne  28800  colperpexlem3  28809  mideulem2  28811  opphllem  28812  midex  28814  opphllem1  28824  opphllem2  28825  opphllem3  28826  opphllem4  28827  opphllem5  28828  opphllem6  28829  outpasch  28832  hlpasch  28833  lnopp2hpgb  28840  colhp  28847  lmieu  28861  hypcgrlem1  28876  hypcgrlem2  28877  lnperpex  28880  trgcopy  28881  trgcopyeulem  28882  iscgra1  28887  cgrane2  28890  cgrane3  28891  cgrane4  28892  cgracgr  28895  cgraid  28896  cgraswap  28897  cgrcgra  28898  cgracom  28899  cgratr  28900  flatcgra  28901  cgraswaplr  28902  cgracol  28905  dfcgra2  28907  sacgr  28908  oacgr  28909  acopy  28910  acopyeu  28911  leagne2  28927  leagne3  28928  cgrg3col4  28930  tgsas1  28931  tgsas2  28933  tgasa1  28935  ttgcontlem1  28962  brbtwn2  28983  axlowdimlem15  29034  axlowdimlem16  29035  axcontlem8  29049  upgrex  29170  edglnl  29221  umgrvad2edg  29291  nbupgr  29422  nbumgrvtx  29424  nbgr2vtx1edg  29428  nbuhgr2vtx1edgb  29430  nbupgrres  29442  cplgr3v  29513  cusgrexilem2  29520  usgredgsscusgredg  29538  1hegrvtxdg1r  29587  1egrvtxdg1r  29589  1egrvtxdg0  29590  pthdadjvtx  29806  pthdlem2lem  29845  wspniunwspnon  30001  umgr2cwwk2dif  30144  3pthdlem1  30244  uhgr3cyclex  30262  upgr4cycl4dv4e  30265  frgr3v  30355  1to3vfriswmgr  30360  frgrwopreglem5a  30391  frgrwopreglem3  30394  frgrhash2wsp  30412  staddi  32326  unidifsnne  32615  ifnefals  32627  coprprop  32781  sgnval2  32817  pmtrcnel  33175  pmtrcnel2  33176  psgnfzto1stlem  33186  cycpmco2lem1  33212  cycpmco2  33219  cyc2fvx  33220  cyc3co2  33226  cycpmrn  33229  tocyccntz  33230  cyc3evpm  33236  cyc3genpmlem  33237  isarchiofld  33285  drngidlhash  33519  qsidomlem2  33538  ssdifidlprm  33543  mxidlnzr  33552  drng0mxidl  33561  drngmxidl  33562  qsdrng  33582  rsprprmprmidl  33607  deg1prod  33668  vietadeg1  33747  ply1annnr  33873  constrrtll  33901  constrrtlc1  33902  constrrtcclem  33904  constrrtcc  33905  constrfin  33916  constrelextdg2  33917  cos9thpiminplylem3  33954  1smat1  33974  submateqlem1  33977  ordtconnlem1  34094  esumrnmpt2  34238  cntnevol  34398  signstfveq0a  34746  repr0  34781  reprlt  34789  reprinfz1  34792  cusgredgex  35329  2cycl2d  35346  acycgr1v  35356  derangenlem  35378  subfacp1lem1  35386  subfacp1lem3  35389  subfacp1lem5  35391  fmlasucdisj  35606  dfrdg4  36158  ifscgr  36251  cgrxfr  36262  btwnconn1lem8  36301  btwnconn3  36310  segcon2  36312  broutsideof3  36333  outsideoftr  36336  outsideofeq  36337  outsideofeu  36338  lineunray  36354  lineelsb2  36355  linethru  36360  unbdqndv2lem2  36723  knoppndvlem1  36725  knoppndvlem2  36726  knoppndvlem7  36731  knoppndvlem14  36738  bj-bary1lem  37528  bj-bary1lem1  37529  bj-bary1  37530  finxpreclem2  37608  finxp1o  37610  finxpreclem6  37614  fin2solem  37820  poimirlem9  37843  poimirlem15  37849  poimirlem20  37854  poimirlem24  37858  poimirlem25  37859  poimirlem27  37861  itg2addnclem2  37886  ftc1cnnc  37906  heibor1lem  38023  maxidln0  38259  lshpnelb  39323  lsatssn0  39341  lsatcv0  39370  lsat0cv  39372  lsatexch1  39385  l1cvat  39394  atlen0  39649  cvlsupr2  39682  atcvrj2b  39771  2atlt  39778  atbtwn  39785  3noncolr2  39788  4noncolr3  39792  3dimlem3  39800  3dimlem3OLDN  39801  3dimlem4  39803  3dimlem4OLDN  39804  3dim2  39807  1cvratex  39812  1cvrat  39815  ps-1  39816  ps-2  39817  hlatexch4  39820  3atlem4  39825  3atlem6  39827  4atlem0ae  39933  4atlem0be  39934  dalemccnedd  40026  dalemrotps  40030  dalem21  40033  dalem23  40035  dalem27  40038  dalem41  40052  dalem44  40055  dalem54  40065  lnatexN  40118  lnjatN  40119  llnexchb2lem  40207  llnexchb2  40208  lhpn0  40343  lhpexle3lem  40350  lhpmatb  40370  4atexlemswapqr  40402  4atexlemc  40408  4atexlemnclw  40409  4atexlemcnd  40411  4atexlemex4  40412  4atexlemex6  40413  4atex  40415  trlat  40508  trlval4  40527  cdlemc5  40534  cdlemd4  40540  cdlemd7  40543  cdlemd9  40545  cdleme0e  40556  cdleme3b  40568  cdleme3c  40569  cdleme3e  40571  cdleme3h  40574  cdleme7aa  40581  cdleme7e  40586  cdleme7ga  40587  cdleme9  40592  cdleme11c  40600  cdleme11e  40602  cdleme11fN  40603  cdleme11h  40605  cdleme11j  40606  cdleme11k  40607  cdleme15b  40614  cdleme15c  40615  cdleme17c  40627  cdleme18b  40631  cdlemesner  40635  cdleme20zN  40640  cdleme19c  40644  cdleme19d  40645  cdleme19e  40646  cdleme20m  40662  cdleme21a  40664  cdleme21b  40665  cdleme21c  40666  cdleme22f2  40686  cdleme28b  40710  cdleme36a  40799  cdleme36m  40800  cdleme41sn4aw  40814  cdleme43bN  40829  cdleme43dN  40831  cdleme46f2g2  40832  cdleme46f2g1  40833  cdleme4gfv  40846  cdlemeg46nlpq  40856  cdlemeg46req  40868  cdlemeg46fgN  40873  cdlemf1  40900  cdlemg8b  40967  cdlemg9a  40971  cdlemg12g  40988  cdlemg12  40989  cdlemg13a  40990  cdlemg17pq  41011  cdlemg18a  41017  cdlemg18c  41019  cdlemg19a  41022  cdlemg19  41023  cdlemg21  41025  cdlemg31b0N  41033  cdlemg31b0a  41034  cdlemg31c  41038  cdlemg33b0  41040  cdlemg33c0  41041  trlcone  41067  cdlemg42  41068  cdlemg44a  41070  cdlemg46  41074  cdlemh1  41154  cdlemh2  41155  cdlemh  41156  cdlemj3  41162  cdlemk3  41172  cdlemki  41180  cdlemksv2  41186  cdlemk12  41189  cdlemk14  41193  cdlemk15  41194  cdlemk7u  41209  cdlemk11u  41210  cdlemk12u  41211  cdlemk21N  41212  cdlemk20  41213  cdlemk22  41232  cdlemk26-3  41245  cdlemk27-3  41246  cdlemk28-3  41247  cdlemkfid3N  41264  cdlemk11ta  41268  cdlemk47  41288  cdlemk54  41297  dia2dimlem1  41403  dochsat  41722  dochshpncl  41723  lclkrlem2b  41847  lcfrlem21  41902  baerlem5amN  42055  baerlem5bmN  42056  baerlem5abmN  42057  mapdindp4  42062  mapdheq2  42068  mapdheq2biN  42069  mapdh6aN  42074  mapdh6dN  42078  mapdh6eN  42079  mapdh6hN  42082  mapdh7eN  42087  mapdh7dN  42089  mapdh7fN  42090  mapdh8ab  42116  mapdh8ad  42118  mapdh8e  42123  mapdh9a  42128  mapdh9aOLDN  42129  hdmap1l6a  42148  hdmap1l6d  42152  hdmap1l6e  42153  hdmap1l6h  42156  hdmap1eulem  42161  hdmap1eulemOLDN  42162  hdmapval0  42172  hdmapeveclem  42173  hdmapval3lemN  42176  hdmap10lem  42178  hdmap11lem1  42180  hdmaprnlem3N  42189  hdmaprnlem9N  42196  hdmaprnlem3eN  42197  fzne2d  42313  lcmineqlem11  42372  3lexlogpow5ineq1  42387  3lexlogpow5ineq2  42388  3lexlogpow5ineq4  42389  3lexlogpow5ineq3  42390  3lexlogpow2ineq1  42391  3lexlogpow2ineq2  42392  3lexlogpow5ineq5  42393  aks4d1lem1  42395  dvrelog2b  42399  dvrelogpow2b  42401  aks4d1p1p3  42402  aks4d1p1p2  42403  aks4d1p1p4  42404  aks4d1p1p6  42406  aks4d1p1p7  42407  aks4d1p1p5  42408  aks4d1p1  42409  aks4d1p2  42410  aks4d1p3  42411  aks4d1p5  42413  aks4d1p6  42414  aks4d1p7d1  42415  aks4d1p7  42416  aks4d1p8d3  42419  aks4d1p8  42420  aks4d1p9  42421  fldhmf1  42423  aks6d1c2p2  42452  hashscontpow  42455  aks6d1c3  42456  aks6d1c5lem2  42471  2np3bcnp1  42477  2ap1caineq  42478  sticksstones1  42479  sticksstones2  42480  sticksstones10  42488  sticksstones12a  42490  sticksstones12  42491  sticksstones22  42501  aks6d1c6lem4  42506  aks6d1c7lem2  42514  unitscyglem2  42529  unitscyglem4  42531  aks5lem8  42534  xppss12  42564  mhpind  42915  jm2.26lem3  43321  rpnnen3lem  43351  rpnnen3  43352  imo72b2lem2  44486  imo72b2  44491  mnuprdlem1  44591  bcc0  44659  chordthmALT  45251  fnchoice  45352  refsum2cnlem1  45360  xrleneltd  45645  xrltned  45679  infleinf  45693  reclt0  45712  icoiccdif  45847  ressiooinf  45880  limcresiooub  45963  limcleqr  45965  limclner  45972  climxrre  46071  icccncfext  46208  cncfiooiccre  46216  dvnxpaek  46263  stoweidlem43  46364  stirlinglem5  46399  stirlinglem7  46401  dirkercncflem1  46424  fourierdlem24  46452  fourierdlem32  46460  fourierdlem33  46461  fourierdlem34  46462  fourierdlem35  46463  fourierdlem46  46473  fourierdlem48  46475  fourierdlem49  46476  fourierdlem64  46491  fourierdlem65  46492  fourierdlem74  46501  fourierdlem76  46503  fourierdlem79  46506  fourierdlem81  46508  fourierdlem91  46518  fourierdlem102  46529  fourierdlem114  46541  etransclem15  46570  etransclem24  46579  sge0rpcpnf  46742  sge0isum  46748  pimrecltpos  47029  m1modne  47671  minusmod5ne  47672  m1modnep2mod  47675  modmknepk  47685  modm2nep1  47689  modm1nep2  47691  setsnidel  47700  odz2prm2pw  47886  fmtnoprmfac1lem  47887  fmtnoprmfac1  47888  fmtnoprmfac2  47890  lighneallem1  47928  lighneallem3  47930  perfectALTVlem2  48045  usgrgrtrirex  48273  isubgr3stgrlem6  48294  gpgusgralem  48379  gpg3nbgrvtx0  48399  pgnioedg1  48431  pgnioedg2  48432  pgnioedg5  48435  nnsgrpnmnd  48501  lvecpsslmod  48830  affinecomb1  49025  affinecomb2  49026  1subrec1sub  49028  rrx2plord2  49045  line  49055  rrxline  49057  eenglngeehlnmlem2  49061  rrx2vlinest  49064  line2xlem  49076  2itscp  49104