Theorem necomd 2987

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

Syntax hints:   → wi 4   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  difsnb  4762  0nelop  5444  xpdifid  6126  f1ounsn  7218  resf1extb  7876  difsnen  8987  fofinf1o  9232  en2eleq  9918  en2other2  9919  ackbij1lem15  10143  infpssrlem5  10217  fin23lem24  10232  fin23lem31  10253  isf32lem9  10271  canthnumlem  10559  canthp1lem2  10564  npomex  10907  ltned  11269  lt0ne0  11603  recgt0  11987  zneo  12575  xrltne  13077  supxrbnd  13243  flltnz  13731  seqf1olem1  13964  nn0opthi  14193  hashtpg  14408  hash7g  14409  hashge3el3dif  14410  cats1un  14644  sumtp  15672  geoserg  15789  geolim  15793  geolim2  15794  tanadd  16092  ruclem6  16160  ruclem7  16161  isprm2lem  16608  isprm5  16634  oddprm  16738  pcmpt  16820  cshwshashlem3  17025  resshom  17338  ressco  17339  mrissmrcd  17563  rescco  17756  estrres  18062  chnccat  18549  chnrev  18550  chnpof1  18553  smndex2dnrinv  18840  pmtrprfv  19382  symggen  19399  dprdcntz  19939  dprdres  19959  ablfac1b  20001  01eq0ringOLD  20464  nrhmzr  20470  ornglmullt  20802  orngrmullt  20803  orngmullt  20804  ofldlt1  20808  lbspss  21034  lspsnnecom  21074  lspindp2l  21089  lspindp2  21090  islbs3  21110  lbsextlem4  21116  lidlnz  21197  ofldchr  21531  uvcf1  21747  frlmup2  21754  psrridm  21918  coe1tmfv2  22217  coe1tmmul  22219  dmatmul  22441  mdetralt  22552  mdetunilem2  22557  mdetunilem6  22561  mdetunilem7  22562  maducoeval2  22584  madurid  22588  fvmptnn04ifa  22794  en2top  22929  cmpfi  23352  snfil  23808  tsmsfbas  24072  zcld  24758  iccpnfhmeo  24899  xrhmeo  24900  evth  24914  minveclem3b  25384  i1fres  25662  dvcnvlem  25936  ig1peu  26136  ig1pdvds  26141  aaliou3lem9  26314  taylthlem2  26338  taylthlem2OLD  26339  abelthlem2  26398  abelthlem7  26404  cos02pilt1  26491  tanregt0  26504  logcj  26571  argimgt0  26577  dvloglem  26613  logf1o2  26615  logbrec  26748  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  ang180lem4  26778  ang180lem5  26779  ang180  26780  isosctrlem3  26786  ssscongptld  26788  affineequivne  26793  angpieqvdlem  26794  angpieqvdlem2  26795  angpieqvd  26797  chordthmlem  26798  chordthmlem2  26799  chordthm  26803  asinneg  26852  ppiltx  27143  perfectlem2  27197  lgsneg  27288  lgsqr  27318  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem3  27349  lgsquad2  27353  2lgsoddprm  27383  dchrisum0flblem1  27475  noseponlem  27632  nosep1o  27649  nosep2o  27650  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  lesrec  27795  0elright  27908  tgbtwnouttr  28569  tgifscgr  28580  tgcgrxfr  28590  tglngval  28623  tgfscgr  28640  tgbtwnconn1lem3  28646  tgbtwnconn3  28649  legtrid  28663  hltr  28682  hlbtwn  28683  btwnhl1  28684  btwnhl  28686  hlcgrex  28688  hlcgreulem  28689  lncom  28694  tgisline  28699  tglineeltr  28703  tglineelsb2  28704  tglinecom  28707  tglinethru  28708  ncolncol  28718  coltr  28719  coltr3  28720  symquadlem  28761  midexlem  28764  ragcol  28771  ragcgr  28779  perpneq  28786  footexALT  28790  footexlem1  28791  footexlem2  28792  foot  28794  footne  28795  colperpexlem3  28804  mideulem2  28806  opphllem  28807  midex  28809  opphllem1  28819  opphllem2  28820  opphllem3  28821  opphllem4  28822  opphllem5  28823  opphllem6  28824  outpasch  28827  hlpasch  28828  lnopp2hpgb  28835  colhp  28842  lmieu  28856  hypcgrlem1  28871  hypcgrlem2  28872  lnperpex  28875  trgcopy  28876  trgcopyeulem  28877  iscgra1  28882  cgrane2  28885  cgrane3  28886  cgrane4  28887  cgracgr  28890  cgraid  28891  cgraswap  28892  cgrcgra  28893  cgracom  28894  cgratr  28895  flatcgra  28896  cgraswaplr  28897  cgracol  28900  dfcgra2  28902  sacgr  28903  oacgr  28904  acopy  28905  acopyeu  28906  leagne2  28922  leagne3  28923  cgrg3col4  28925  tgsas1  28926  tgsas2  28928  tgasa1  28930  ttgcontlem1  28957  brbtwn2  28978  axlowdimlem15  29029  axlowdimlem16  29030  axcontlem8  29044  upgrex  29165  edglnl  29216  umgrvad2edg  29286  nbupgr  29417  nbumgrvtx  29419  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  nbupgrres  29437  cplgr3v  29508  cusgrexilem2  29515  usgredgsscusgredg  29533  1hegrvtxdg1r  29582  1egrvtxdg1r  29584  1egrvtxdg0  29585  pthdadjvtx  29801  pthdlem2lem  29840  wspniunwspnon  29996  umgr2cwwk2dif  30139  3pthdlem1  30239  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  frgr3v  30350  1to3vfriswmgr  30355  frgrwopreglem5a  30386  frgrwopreglem3  30389  frgrhash2wsp  30407  staddi  32321  unidifsnne  32611  ifnefals  32623  coprprop  32778  sgnval2  32814  pmtrcnel  33171  pmtrcnel2  33172  psgnfzto1stlem  33182  cycpmco2lem1  33208  cycpmco2  33215  cyc2fvx  33216  cyc3co2  33222  cycpmrn  33225  tocyccntz  33226  cyc3evpm  33232  cyc3genpmlem  33233  isarchiofld  33281  drngidlhash  33515  qsidomlem2  33534  ssdifidlprm  33539  mxidlnzr  33548  drng0mxidl  33557  drngmxidl  33558  qsdrng  33578  rsprprmprmidl  33603  deg1prod  33664  vietadeg1  33734  ply1annnr  33860  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrfin  33903  constrelextdg2  33904  cos9thpiminplylem3  33941  1smat1  33961  submateqlem1  33964  ordtconnlem1  34081  esumrnmpt2  34225  cntnevol  34385  signstfveq0a  34733  repr0  34768  reprlt  34776  reprinfz1  34779  cusgredgex  35316  2cycl2d  35333  acycgr1v  35343  derangenlem  35365  subfacp1lem1  35373  subfacp1lem3  35376  subfacp1lem5  35378  fmlasucdisj  35593  dfrdg4  36145  ifscgr  36238  cgrxfr  36249  btwnconn1lem8  36288  btwnconn3  36297  segcon2  36299  broutsideof3  36320  outsideoftr  36323  outsideofeq  36324  outsideofeu  36325  lineunray  36341  lineelsb2  36342  linethru  36347  unbdqndv2lem2  36710  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem14  36725  bj-bary1lem  37515  bj-bary1lem1  37516  bj-bary1  37517  finxpreclem2  37595  finxp1o  37597  finxpreclem6  37601  fin2solem  37807  poimirlem9  37830  poimirlem15  37836  poimirlem20  37841  poimirlem24  37845  poimirlem25  37846  poimirlem27  37848  itg2addnclem2  37873  ftc1cnnc  37893  heibor1lem  38010  maxidln0  38246  lshpnelb  39244  lsatssn0  39262  lsatcv0  39291  lsat0cv  39293  lsatexch1  39306  l1cvat  39315  atlen0  39570  cvlsupr2  39603  atcvrj2b  39692  2atlt  39699  atbtwn  39706  3noncolr2  39709  4noncolr3  39713  3dimlem3  39721  3dimlem3OLDN  39722  3dimlem4  39724  3dimlem4OLDN  39725  3dim2  39728  1cvratex  39733  1cvrat  39736  ps-1  39737  ps-2  39738  hlatexch4  39741  3atlem4  39746  3atlem6  39748  4atlem0ae  39854  4atlem0be  39855  dalemccnedd  39947  dalemrotps  39951  dalem21  39954  dalem23  39956  dalem27  39959  dalem41  39973  dalem44  39976  dalem54  39986  lnatexN  40039  lnjatN  40040  llnexchb2lem  40128  llnexchb2  40129  lhpn0  40264  lhpexle3lem  40271  lhpmatb  40291  4atexlemswapqr  40323  4atexlemc  40329  4atexlemnclw  40330  4atexlemcnd  40332  4atexlemex4  40333  4atexlemex6  40334  4atex  40336  trlat  40429  trlval4  40448  cdlemc5  40455  cdlemd4  40461  cdlemd7  40464  cdlemd9  40466  cdleme0e  40477  cdleme3b  40489  cdleme3c  40490  cdleme3e  40492  cdleme3h  40495  cdleme7aa  40502  cdleme7e  40507  cdleme7ga  40508  cdleme9  40513  cdleme11c  40521  cdleme11e  40523  cdleme11fN  40524  cdleme11h  40526  cdleme11j  40527  cdleme11k  40528  cdleme15b  40535  cdleme15c  40536  cdleme17c  40548  cdleme18b  40552  cdlemesner  40556  cdleme20zN  40561  cdleme19c  40565  cdleme19d  40566  cdleme19e  40567  cdleme20m  40583  cdleme21a  40585  cdleme21b  40586  cdleme21c  40587  cdleme22f2  40607  cdleme28b  40631  cdleme36a  40720  cdleme36m  40721  cdleme41sn4aw  40735  cdleme43bN  40750  cdleme43dN  40752  cdleme46f2g2  40753  cdleme46f2g1  40754  cdleme4gfv  40767  cdlemeg46nlpq  40777  cdlemeg46req  40789  cdlemeg46fgN  40794  cdlemf1  40821  cdlemg8b  40888  cdlemg9a  40892  cdlemg12g  40909  cdlemg12  40910  cdlemg13a  40911  cdlemg17pq  40932  cdlemg18a  40938  cdlemg18c  40940  cdlemg19a  40943  cdlemg19  40944  cdlemg21  40946  cdlemg31b0N  40954  cdlemg31b0a  40955  cdlemg31c  40959  cdlemg33b0  40961  cdlemg33c0  40962  trlcone  40988  cdlemg42  40989  cdlemg44a  40991  cdlemg46  40995  cdlemh1  41075  cdlemh2  41076  cdlemh  41077  cdlemj3  41083  cdlemk3  41093  cdlemki  41101  cdlemksv2  41107  cdlemk12  41110  cdlemk14  41114  cdlemk15  41115  cdlemk7u  41130  cdlemk11u  41131  cdlemk12u  41132  cdlemk21N  41133  cdlemk20  41134  cdlemk22  41153  cdlemk26-3  41166  cdlemk27-3  41167  cdlemk28-3  41168  cdlemkfid3N  41185  cdlemk11ta  41189  cdlemk47  41209  cdlemk54  41218  dia2dimlem1  41324  dochsat  41643  dochshpncl  41644  lclkrlem2b  41768  lcfrlem21  41823  baerlem5amN  41976  baerlem5bmN  41977  baerlem5abmN  41978  mapdindp4  41983  mapdheq2  41989  mapdheq2biN  41990  mapdh6aN  41995  mapdh6dN  41999  mapdh6eN  42000  mapdh6hN  42003  mapdh7eN  42008  mapdh7dN  42010  mapdh7fN  42011  mapdh8ab  42037  mapdh8ad  42039  mapdh8e  42044  mapdh9a  42049  mapdh9aOLDN  42050  hdmap1l6a  42069  hdmap1l6d  42073  hdmap1l6e  42074  hdmap1l6h  42077  hdmap1eulem  42082  hdmap1eulemOLDN  42083  hdmapval0  42093  hdmapeveclem  42094  hdmapval3lemN  42097  hdmap10lem  42099  hdmap11lem1  42101  hdmaprnlem3N  42110  hdmaprnlem9N  42117  hdmaprnlem3eN  42118  fzne2d  42234  lcmineqlem11  42293  3lexlogpow5ineq1  42308  3lexlogpow5ineq2  42309  3lexlogpow5ineq4  42310  3lexlogpow5ineq3  42311  3lexlogpow2ineq1  42312  3lexlogpow2ineq2  42313  3lexlogpow5ineq5  42314  aks4d1lem1  42316  dvrelog2b  42320  dvrelogpow2b  42322  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8d3  42340  aks4d1p8  42341  aks4d1p9  42342  fldhmf1  42344  aks6d1c2p2  42373  hashscontpow  42376  aks6d1c3  42377  aks6d1c5lem2  42392  2np3bcnp1  42398  2ap1caineq  42399  sticksstones1  42400  sticksstones2  42401  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones22  42422  aks6d1c6lem4  42427  aks6d1c7lem2  42435  unitscyglem2  42450  unitscyglem4  42452  aks5lem8  42455  xppss12  42485  mhpind  42837  jm2.26lem3  43243  rpnnen3lem  43273  rpnnen3  43274  imo72b2lem2  44408  imo72b2  44413  mnuprdlem1  44513  bcc0  44581  chordthmALT  45173  fnchoice  45274  refsum2cnlem1  45282  xrleneltd  45568  xrltned  45602  infleinf  45616  reclt0  45635  icoiccdif  45770  ressiooinf  45803  limcresiooub  45886  limcleqr  45888  limclner  45895  climxrre  45994  icccncfext  46131  cncfiooiccre  46139  dvnxpaek  46186  stoweidlem43  46287  stirlinglem5  46322  stirlinglem7  46324  dirkercncflem1  46347  fourierdlem24  46375  fourierdlem32  46383  fourierdlem33  46384  fourierdlem34  46385  fourierdlem35  46386  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem64  46414  fourierdlem65  46415  fourierdlem74  46424  fourierdlem76  46426  fourierdlem79  46429  fourierdlem81  46431  fourierdlem91  46441  fourierdlem102  46452  fourierdlem114  46464  etransclem15  46493  etransclem24  46502  sge0rpcpnf  46665  sge0isum  46671  pimrecltpos  46952  m1modne  47594  minusmod5ne  47595  m1modnep2mod  47598  modmknepk  47608  modm2nep1  47612  modm1nep2  47614  setsnidel  47623  odz2prm2pw  47809  fmtnoprmfac1lem  47810  fmtnoprmfac1  47811  fmtnoprmfac2  47813  lighneallem1  47851  lighneallem3  47853  perfectALTVlem2  47968  usgrgrtrirex  48196  isubgr3stgrlem6  48217  gpgusgralem  48302  gpg3nbgrvtx0  48322  pgnioedg1  48354  pgnioedg2  48355  pgnioedg5  48358  nnsgrpnmnd  48424  lvecpsslmod  48753  affinecomb1  48948  affinecomb2  48949  1subrec1sub  48951  rrx2plord2  48968  line  48978  rrxline  48980  eenglngeehlnmlem2  48984  rrx2vlinest  48987  line2xlem  48999  2itscp  49027