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  4752  0nelop  5451  xpdifid  6133  f1ounsn  7227  resf1extb  7885  difsnen  8997  fofinf1o  9242  en2eleq  9930  en2other2  9931  ackbij1lem15  10155  infpssrlem5  10229  fin23lem24  10244  fin23lem31  10265  isf32lem9  10283  canthnumlem  10571  canthp1lem2  10576  npomex  10919  ltned  11282  lt0ne0  11616  recgt0  12001  zneo  12612  xrltne  13114  supxrbnd  13280  flltnz  13770  seqf1olem1  14003  nn0opthi  14232  hashtpg  14447  hash7g  14448  hashge3el3dif  14449  cats1un  14683  sumtp  15711  geoserg  15831  geolim  15835  geolim2  15836  tanadd  16134  ruclem6  16202  ruclem7  16203  isprm2lem  16650  isprm5  16677  oddprm  16781  pcmpt  16863  cshwshashlem3  17068  resshom  17381  ressco  17382  mrissmrcd  17606  rescco  17799  estrres  18105  chnccat  18592  chnrev  18593  chnpof1  18596  smndex2dnrinv  18886  pmtrprfv  19428  symggen  19445  dprdcntz  19985  dprdres  20005  ablfac1b  20047  01eq0ringOLD  20508  nrhmzr  20514  ornglmullt  20846  orngrmullt  20847  orngmullt  20848  ofldlt1  20852  lbspss  21077  lspsnnecom  21117  lspindp2l  21132  lspindp2  21133  islbs3  21153  lbsextlem4  21159  lidlnz  21240  ofldchr  21556  uvcf1  21772  frlmup2  21779  psrridm  21941  coe1tmfv2  22240  coe1tmmul  22242  dmatmul  22462  mdetralt  22573  mdetunilem2  22578  mdetunilem6  22582  mdetunilem7  22583  maducoeval2  22605  madurid  22609  fvmptnn04ifa  22815  en2top  22950  cmpfi  23373  snfil  23829  tsmsfbas  24093  zcld  24779  iccpnfhmeo  24912  xrhmeo  24913  evth  24926  minveclem3b  25395  i1fres  25672  dvcnvlem  25943  ig1peu  26140  ig1pdvds  26145  aaliou3lem9  26316  taylthlem2  26339  abelthlem2  26397  abelthlem7  26403  cos02pilt1  26490  tanregt0  26503  logcj  26570  argimgt0  26576  dvloglem  26612  logf1o2  26614  logbrec  26746  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  ang180lem4  26776  ang180lem5  26777  ang180  26778  isosctrlem3  26784  ssscongptld  26786  affineequivne  26791  angpieqvdlem  26792  angpieqvdlem2  26793  angpieqvd  26795  chordthmlem  26796  chordthmlem2  26797  chordthm  26801  asinneg  26850  ppiltx  27140  perfectlem2  27193  lgsneg  27284  lgsqr  27314  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem3  27345  lgsquad2  27349  2lgsoddprm  27379  dchrisum0flblem1  27471  noseponlem  27628  nosep1o  27645  nosep2o  27646  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  lesrec  27791  0elright  27904  tgbtwnouttr  28565  tgifscgr  28576  tgcgrxfr  28586  tglngval  28619  tgfscgr  28636  tgbtwnconn1lem3  28642  tgbtwnconn3  28645  legtrid  28659  hltr  28678  hlbtwn  28679  btwnhl1  28680  btwnhl  28682  hlcgrex  28684  hlcgreulem  28685  lncom  28690  tgisline  28695  tglineeltr  28699  tglineelsb2  28700  tglinecom  28703  tglinethru  28704  ncolncol  28714  coltr  28715  coltr3  28716  symquadlem  28757  midexlem  28760  ragcol  28767  ragcgr  28775  perpneq  28782  footexALT  28786  footexlem1  28787  footexlem2  28788  foot  28790  footne  28791  colperpexlem3  28800  mideulem2  28802  opphllem  28803  midex  28805  opphllem1  28815  opphllem2  28816  opphllem3  28817  opphllem4  28818  opphllem5  28819  opphllem6  28820  outpasch  28823  hlpasch  28824  lnopp2hpgb  28831  colhp  28838  lmieu  28852  hypcgrlem1  28867  hypcgrlem2  28868  lnperpex  28871  trgcopy  28872  trgcopyeulem  28873  iscgra1  28878  cgrane2  28881  cgrane3  28882  cgrane4  28883  cgracgr  28886  cgraid  28887  cgraswap  28888  cgrcgra  28889  cgracom  28890  cgratr  28891  flatcgra  28892  cgraswaplr  28893  cgracol  28896  dfcgra2  28898  sacgr  28899  oacgr  28900  acopy  28901  acopyeu  28902  leagne2  28918  leagne3  28919  cgrg3col4  28921  tgsas1  28922  tgsas2  28924  tgasa1  28926  ttgcontlem1  28953  brbtwn2  28974  axlowdimlem15  29025  axlowdimlem16  29026  axcontlem8  29040  upgrex  29161  edglnl  29212  umgrvad2edg  29282  nbupgr  29413  nbumgrvtx  29415  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nbupgrres  29433  cplgr3v  29504  cusgrexilem2  29511  usgredgsscusgredg  29528  1hegrvtxdg1r  29577  1egrvtxdg1r  29579  1egrvtxdg0  29580  pthdadjvtx  29796  pthdlem2lem  29835  wspniunwspnon  29991  umgr2cwwk2dif  30134  3pthdlem1  30234  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  frgr3v  30345  1to3vfriswmgr  30350  frgrwopreglem5a  30381  frgrwopreglem3  30384  frgrhash2wsp  30402  staddi  32317  unidifsnne  32606  ifnefals  32618  coprprop  32772  sgnval2  32808  pmtrcnel  33150  pmtrcnel2  33151  psgnfzto1stlem  33161  cycpmco2lem1  33187  cycpmco2  33194  cyc2fvx  33195  cyc3co2  33201  cycpmrn  33204  tocyccntz  33205  cyc3evpm  33211  cyc3genpmlem  33212  isarchiofld  33260  drngidlhash  33494  qsidomlem2  33513  ssdifidlprm  33518  mxidlnzr  33527  drng0mxidl  33536  drngmxidl  33537  qsdrng  33557  rsprprmprmidl  33582  deg1prod  33643  vietadeg1  33722  ply1annnr  33847  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrfin  33890  constrelextdg2  33891  cos9thpiminplylem3  33928  1smat1  33948  submateqlem1  33951  ordtconnlem1  34068  esumrnmpt2  34212  cntnevol  34372  signstfveq0a  34720  repr0  34755  reprlt  34763  reprinfz1  34766  cusgredgex  35304  2cycl2d  35321  acycgr1v  35331  derangenlem  35353  subfacp1lem1  35361  subfacp1lem3  35364  subfacp1lem5  35366  fmlasucdisj  35581  dfrdg4  36133  ifscgr  36226  cgrxfr  36237  btwnconn1lem8  36276  btwnconn3  36285  segcon2  36287  broutsideof3  36308  outsideoftr  36311  outsideofeq  36312  outsideofeu  36313  lineunray  36329  lineelsb2  36330  linethru  36335  mh-inf3f1  36723  mh-inf3sn  36724  unbdqndv2lem2  36770  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem14  36785  bj-bary1lem  37624  bj-bary1lem1  37625  bj-bary1  37626  finxpreclem2  37706  finxp1o  37708  finxpreclem6  37712  fin2solem  37927  poimirlem9  37950  poimirlem15  37956  poimirlem20  37961  poimirlem24  37965  poimirlem25  37966  poimirlem27  37968  itg2addnclem2  37993  ftc1cnnc  38013  heibor1lem  38130  maxidln0  38366  lshpnelb  39430  lsatssn0  39448  lsatcv0  39477  lsat0cv  39479  lsatexch1  39492  l1cvat  39501  atlen0  39756  cvlsupr2  39789  atcvrj2b  39878  2atlt  39885  atbtwn  39892  3noncolr2  39895  4noncolr3  39899  3dimlem3  39907  3dimlem3OLDN  39908  3dimlem4  39910  3dimlem4OLDN  39911  3dim2  39914  1cvratex  39919  1cvrat  39922  ps-1  39923  ps-2  39924  hlatexch4  39927  3atlem4  39932  3atlem6  39934  4atlem0ae  40040  4atlem0be  40041  dalemccnedd  40133  dalemrotps  40137  dalem21  40140  dalem23  40142  dalem27  40145  dalem41  40159  dalem44  40162  dalem54  40172  lnatexN  40225  lnjatN  40226  llnexchb2lem  40314  llnexchb2  40315  lhpn0  40450  lhpexle3lem  40457  lhpmatb  40477  4atexlemswapqr  40509  4atexlemc  40515  4atexlemnclw  40516  4atexlemcnd  40518  4atexlemex4  40519  4atexlemex6  40520  4atex  40522  trlat  40615  trlval4  40634  cdlemc5  40641  cdlemd4  40647  cdlemd7  40650  cdlemd9  40652  cdleme0e  40663  cdleme3b  40675  cdleme3c  40676  cdleme3e  40678  cdleme3h  40681  cdleme7aa  40688  cdleme7e  40693  cdleme7ga  40694  cdleme9  40699  cdleme11c  40707  cdleme11e  40709  cdleme11fN  40710  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme15b  40721  cdleme15c  40722  cdleme17c  40734  cdleme18b  40738  cdlemesner  40742  cdleme20zN  40747  cdleme19c  40751  cdleme19d  40752  cdleme19e  40753  cdleme20m  40769  cdleme21a  40771  cdleme21b  40772  cdleme21c  40773  cdleme22f2  40793  cdleme28b  40817  cdleme36a  40906  cdleme36m  40907  cdleme41sn4aw  40921  cdleme43bN  40936  cdleme43dN  40938  cdleme46f2g2  40939  cdleme46f2g1  40940  cdleme4gfv  40953  cdlemeg46nlpq  40963  cdlemeg46req  40975  cdlemeg46fgN  40980  cdlemf1  41007  cdlemg8b  41074  cdlemg9a  41078  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg17pq  41118  cdlemg18a  41124  cdlemg18c  41126  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg31b0N  41140  cdlemg31b0a  41141  cdlemg31c  41145  cdlemg33b0  41147  cdlemg33c0  41148  trlcone  41174  cdlemg42  41175  cdlemg44a  41177  cdlemg46  41181  cdlemh1  41261  cdlemh2  41262  cdlemh  41263  cdlemj3  41269  cdlemk3  41279  cdlemki  41287  cdlemksv2  41293  cdlemk12  41296  cdlemk14  41300  cdlemk15  41301  cdlemk7u  41316  cdlemk11u  41317  cdlemk12u  41318  cdlemk21N  41319  cdlemk20  41320  cdlemk22  41339  cdlemk26-3  41352  cdlemk27-3  41353  cdlemk28-3  41354  cdlemkfid3N  41371  cdlemk11ta  41375  cdlemk47  41395  cdlemk54  41404  dia2dimlem1  41510  dochsat  41829  dochshpncl  41830  lclkrlem2b  41954  lcfrlem21  42009  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdindp4  42169  mapdheq2  42175  mapdheq2biN  42176  mapdh6aN  42181  mapdh6dN  42185  mapdh6eN  42186  mapdh6hN  42189  mapdh7eN  42194  mapdh7dN  42196  mapdh7fN  42197  mapdh8ab  42223  mapdh8ad  42225  mapdh8e  42230  mapdh9a  42235  mapdh9aOLDN  42236  hdmap1l6a  42255  hdmap1l6d  42259  hdmap1l6e  42260  hdmap1l6h  42263  hdmap1eulem  42268  hdmap1eulemOLDN  42269  hdmapval0  42279  hdmapeveclem  42280  hdmapval3lemN  42283  hdmap10lem  42285  hdmap11lem1  42287  hdmaprnlem3N  42296  hdmaprnlem9N  42303  hdmaprnlem3eN  42304  fzne2d  42419  lcmineqlem11  42478  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  fldhmf1  42529  aks6d1c2p2  42558  hashscontpow  42561  aks6d1c3  42562  aks6d1c5lem2  42577  2np3bcnp1  42583  2ap1caineq  42584  sticksstones1  42585  sticksstones2  42586  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem4  42612  aks6d1c7lem2  42620  unitscyglem2  42635  unitscyglem4  42637  aks5lem8  42640  xppss12  42670  mhpind  43027  jm2.26lem3  43429  rpnnen3lem  43459  rpnnen3  43460  imo72b2lem2  44594  imo72b2  44599  mnuprdlem1  44699  bcc0  44767  chordthmALT  45359  fnchoice  45460  refsum2cnlem1  45468  xrleneltd  45753  xrltned  45787  infleinf  45801  reclt0  45820  icoiccdif  45954  ressiooinf  45987  limcresiooub  46070  limcleqr  46072  limclner  46079  climxrre  46178  icccncfext  46315  cncfiooiccre  46323  dvnxpaek  46370  stoweidlem43  46471  stirlinglem5  46506  stirlinglem7  46508  dirkercncflem1  46531  fourierdlem24  46559  fourierdlem32  46567  fourierdlem33  46568  fourierdlem34  46569  fourierdlem35  46570  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem91  46625  fourierdlem102  46636  fourierdlem114  46648  etransclem15  46677  etransclem24  46686  sge0rpcpnf  46849  sge0isum  46855  pimrecltpos  47136  m1modne  47796  minusmod5ne  47797  m1modnep2mod  47800  modmknepk  47810  modm2nep1  47814  modm1nep2  47816  setsnidel  47831  odz2prm2pw  48020  fmtnoprmfac1lem  48021  fmtnoprmfac1  48022  fmtnoprmfac2  48024  lighneallem1  48062  lighneallem3  48064  perfectALTVlem2  48192  usgrgrtrirex  48420  isubgr3stgrlem6  48441  gpgusgralem  48526  gpg3nbgrvtx0  48546  pgnioedg1  48578  pgnioedg2  48579  pgnioedg5  48582  nnsgrpnmnd  48648  lvecpsslmod  48977  affinecomb1  49172  affinecomb2  49173  1subrec1sub  49175  rrx2plord2  49192  line  49202  rrxline  49204  eenglngeehlnmlem2  49208  rrx2vlinest  49211  line2xlem  49223  2itscp  49251