Theorem necomd 3013

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

Syntax hints:   → wi 4   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-ne 2959

This theorem is referenced by:  difsnb  4767  0nelop  5466  xpdifid  6153  f1ounsn  7256  resf1extb  7915  difsnen  9031  fofinf1o  9273  en2eleq  9976  en2other2  9977  ackbij1lem15  10200  infpssrlem5  10275  fin23lem24  10290  fin23lem31  10311  isf32lem9  10329  canthnumlem  10617  canthp1lem2  10622  npomex  10965  ltned  11330  lt0ne0  11664  recgt0  12048  zneo  12666  xrltne  13175  supxrbnd  13341  flltnz  13831  seqf1olem1  14064  nn0opthi  14293  hashtpg  14508  hash7g  14509  hashge3el3dif  14510  cats1un  14744  sumtp  15786  geoserg  15906  geolim  15910  geolim2  15911  tanadd  16209  ruclem6  16277  ruclem7  16278  isprm2lem  16725  isprm5  16752  oddprm  16856  pcmpt  16938  cshwshashlem3  17143  resshom  17457  ressco  17458  mrissmrcd  17682  rescco  17875  estrres  18181  chnccat  18668  chnrev  18669  chnpof1  18672  smndex2dnrinv  18962  pmtrprfv  19503  symggen  19520  dprdcntz  20060  dprdres  20080  ablfac1b  20122  01eq0ringOLD  20591  nrhmzr  20597  ornglmullt  20925  orngrmullt  20926  orngmullt  20927  ofldlt1  20931  lbspss  21156  lspsnnecom  21196  lspindp2l  21211  lspindp2  21212  islbs3  21232  lbsextlem4  21238  lidlnz  21319  ofldchr  21635  uvcf1  21851  frlmup2  21858  psrridm  22021  coe1tmfv2  22345  coe1tmmul  22347  dmatmul  22564  mdetralt  22675  mdetunilem2  22680  mdetunilem6  22684  mdetunilem7  22685  maducoeval2  22707  madurid  22711  fvmptnn04ifa  22917  en2top  23052  cmpfi  23475  snfil  23931  tsmsfbas  24195  zcld  24881  iccpnfhmeo  25014  xrhmeo  25015  evth  25028  minveclem3b  25497  i1fres  25774  dvcnvlem  26045  ig1peu  26242  ig1pdvds  26247  aaliou3lem9  26421  taylthlem2  26444  abelthlem2  26502  abelthlem7  26508  cos02pilt1  26598  tanregt0  26611  logcj  26678  argimgt0  26684  dvloglem  26720  logf1o2  26722  logbrec  26854  ang180lem1  26881  ang180lem2  26882  ang180lem3  26883  ang180lem4  26884  ang180lem5  26885  ang180  26886  isosctrlem3  26892  ssscongptld  26894  affineequivne  26899  angpieqvdlem  26900  angpieqvdlem2  26901  angpieqvd  26903  chordthmlem  26904  chordthmlem2  26905  chordthm  26909  asinneg  26958  ppiltx  27248  perfectlem2  27301  lgsneg  27392  lgsqr  27422  lgseisenlem4  27449  lgsquadlem1  27451  lgsquadlem3  27453  lgsquad2  27457  2lgsoddprm  27487  dchrisum0flblem1  27579  noseponlem  27735  nosep1o  27752  nosep2o  27753  nosupbnd2lem1  27786  noinfbnd2lem1  27801  noetasuplem4  27807  noetainflem4  27811  lesrec  27899  0elright  28012  tgbtwnouttr  28673  tgifscgr  28684  tgcgrxfr  28694  tglngval  28727  tgfscgr  28744  tgbtwnconn1lem3  28750  tgbtwnconn3  28753  legtrid  28767  hltr  28786  hlbtwn  28787  btwnhl1  28788  btwnhl  28790  hlcgrex  28792  hlcgreulem  28793  lncom  28798  tgisline  28803  tglineeltr  28807  tglineelsb2  28808  tglinecom  28811  tglinethru  28812  ncolncol  28823  coltr  28824  coltr3  28825  tglnpt3  28830  tglnpt4  28831  symquadlem  28869  midexlem  28872  ragcol  28879  ragcgr  28887  perpneq  28894  footexALT  28898  footexlem1  28899  footexlem2  28900  foot  28902  footne  28903  colperpexlem3  28912  mideulem2  28914  opphllem  28915  midex  28917  opphllem1  28927  opphllem2  28928  opphllem3  28929  opphllem4  28930  opphllem5  28931  opphllem6  28932  outpasch  28935  hlpasch  28936  lnopp2hpgb  28943  colhp  28950  lmieu  28964  hypcgrlem1  28979  hypcgrlem2  28980  lnperpex  28983  trgcopy  28984  trgcopyeulem  28985  lnincplng  28998  plngrotlem1  29001  plngrotlem2  29002  plngrot  29004  lnssplnglem  29005  lnssplng  29006  iscgra1  29011  cgrane2  29014  cgrane3  29015  cgrane4  29016  cgracgr  29019  cgraid  29020  cgraswap  29021  cgrcgra  29022  cgracom  29023  cgratr  29024  flatcgra  29025  cgraswaplr  29026  cgracol  29029  dfcgra2  29031  sacgr  29032  oacgr  29033  acopy  29034  acopyeu  29035  leagne2  29051  leagne3  29052  cgrg3col4  29054  tgsas1  29055  tgsas2  29057  tgasa1  29059  ttgcontlem1  29092  brbtwn2  29113  axlowdimlem15  29164  axlowdimlem16  29165  axcontlem8  29179  upgrex  29300  edglnl  29351  umgrvad2edg  29421  nbupgr  29552  nbumgrvtx  29554  nbgr2vtx1edg  29558  nbuhgr2vtx1edgb  29560  nbupgrres  29572  cplgr3v  29643  cusgrexilem2  29650  usgredgsscusgredg  29667  1hegrvtxdg1r  29716  1egrvtxdg1r  29718  1egrvtxdg0  29719  pthdadjvtx  29935  pthdlem2lem  29974  wspniunwspnon  30130  umgr2cwwk2dif  30273  3pthdlem1  30373  uhgr3cyclex  30391  upgr4cycl4dv4e  30394  frgr3v  30484  1to3vfriswmgr  30489  frgrwopreglem5a  30520  frgrwopreglem3  30523  frgrhash2wsp  30541  staddi  32456  unidifsnne  32741  ifnefals  32753  coprprop  32907  sgnval2  32943  pmtrcnel  33275  pmtrcnel2  33276  psgnfzto1stlem  33286  cycpmco2lem1  33312  cycpmco2  33319  cyc2fvx  33320  cyc3co2  33326  cycpmrn  33329  tocyccntz  33330  cyc3evpm  33336  cyc3genpmlem  33337  isarchiofld  33385  drngidlhash  33623  qsidomlem2  33643  ssdifidlprm  33648  mxidlnzr  33658  drng0mxidl  33667  drngmxidl  33668  qsdrng  33688  dflringlem3  33695  dflring3  33696  dflring4  33697  rsprprmprmidl  33721  deg1prod  33782  vietadeg1  33877  ply1annnr  34002  constrrtll  34030  constrrtlc1  34031  constrrtcclem  34033  constrrtcc  34034  constrfin  34045  constrelextdg2  34046  cos9thpiminplylem3  34083  1smat1  34103  submateqlem1  34106  ordtconnlem1  34223  esumrnmpt2  34367  cntnevol  34527  signstfveq0a  34872  repr0  34907  reprlt  34915  reprinfz1  34918  morleylemrneab  34967  cusgredgex  35477  2cycl2d  35494  acycgr1v  35504  derangenlem  35526  subfacp1lem1  35534  subfacp1lem3  35537  subfacp1lem5  35539  fmlasucdisj  35754  dfrdg4  36306  ifscgr  36399  cgrxfr  36410  btwnconn1lem8  36449  btwnconn3  36458  segcon2  36460  broutsideof3  36481  outsideoftr  36484  outsideofeq  36485  outsideofeu  36486  lineunray  36502  lineelsb2  36503  linethru  36508  mh-inf3f1  36906  mh-inf3sn  36907  unbdqndv2lem2  36953  knoppndvlem1  36955  knoppndvlem2  36956  knoppndvlem7  36961  knoppndvlem14  36968  bj-bary1lem  37807  bj-bary1lem1  37808  bj-bary1  37809  finxpreclem2  37889  finxp1o  37891  finxpreclem6  37895  fin2solem  38110  poimirlem9  38133  poimirlem15  38139  poimirlem20  38144  poimirlem24  38148  poimirlem25  38149  poimirlem27  38151  itg2addnclem2  38176  ftc1cnnc  38196  heibor1lem  38313  maxidln0  38549  lshpnelb  39613  lsatssn0  39631  lsatcv0  39660  lsat0cv  39662  lsatexch1  39675  l1cvat  39684  atlen0  39939  cvlsupr2  39972  atcvrj2b  40061  2atlt  40068  atbtwn  40075  3noncolr2  40078  4noncolr3  40082  3dimlem3  40090  3dimlem3OLDN  40091  3dimlem4  40093  3dimlem4OLDN  40094  3dim2  40097  1cvratex  40102  1cvrat  40105  ps-1  40106  ps-2  40107  hlatexch4  40110  3atlem4  40115  3atlem6  40117  4atlem0ae  40223  4atlem0be  40224  dalemccnedd  40316  dalemrotps  40320  dalem21  40323  dalem23  40325  dalem27  40328  dalem41  40342  dalem44  40345  dalem54  40355  lnatexN  40408  lnjatN  40409  llnexchb2lem  40497  llnexchb2  40498  lhpn0  40633  lhpexle3lem  40640  lhpmatb  40660  4atexlemswapqr  40692  4atexlemc  40698  4atexlemnclw  40699  4atexlemcnd  40701  4atexlemex4  40702  4atexlemex6  40703  4atex  40705  trlat  40798  trlval4  40817  cdlemc5  40824  cdlemd4  40830  cdlemd7  40833  cdlemd9  40835  cdleme0e  40846  cdleme3b  40858  cdleme3c  40859  cdleme3e  40861  cdleme3h  40864  cdleme7aa  40871  cdleme7e  40876  cdleme7ga  40877  cdleme9  40882  cdleme11c  40890  cdleme11e  40892  cdleme11fN  40893  cdleme11h  40895  cdleme11j  40896  cdleme11k  40897  cdleme15b  40904  cdleme15c  40905  cdleme17c  40917  cdleme18b  40921  cdlemesner  40925  cdleme20zN  40930  cdleme19c  40934  cdleme19d  40935  cdleme19e  40936  cdleme20m  40952  cdleme21a  40954  cdleme21b  40955  cdleme21c  40956  cdleme22f2  40976  cdleme28b  41000  cdleme36a  41089  cdleme36m  41090  cdleme41sn4aw  41104  cdleme43bN  41119  cdleme43dN  41121  cdleme46f2g2  41122  cdleme46f2g1  41123  cdleme4gfv  41136  cdlemeg46nlpq  41146  cdlemeg46req  41158  cdlemeg46fgN  41163  cdlemf1  41190  cdlemg8b  41257  cdlemg9a  41261  cdlemg12g  41278  cdlemg12  41279  cdlemg13a  41280  cdlemg17pq  41301  cdlemg18a  41307  cdlemg18c  41309  cdlemg19a  41312  cdlemg19  41313  cdlemg21  41315  cdlemg31b0N  41323  cdlemg31b0a  41324  cdlemg31c  41328  cdlemg33b0  41330  cdlemg33c0  41331  trlcone  41357  cdlemg42  41358  cdlemg44a  41360  cdlemg46  41364  cdlemh1  41444  cdlemh2  41445  cdlemh  41446  cdlemj3  41452  cdlemk3  41462  cdlemki  41470  cdlemksv2  41476  cdlemk12  41479  cdlemk14  41483  cdlemk15  41484  cdlemk7u  41499  cdlemk11u  41500  cdlemk12u  41501  cdlemk21N  41502  cdlemk20  41503  cdlemk22  41522  cdlemk26-3  41535  cdlemk27-3  41536  cdlemk28-3  41537  cdlemkfid3N  41554  cdlemk11ta  41558  cdlemk47  41578  cdlemk54  41587  dia2dimlem1  41693  dochsat  42012  dochshpncl  42013  lclkrlem2b  42137  lcfrlem21  42192  baerlem5amN  42345  baerlem5bmN  42346  baerlem5abmN  42347  mapdindp4  42352  mapdheq2  42358  mapdheq2biN  42359  mapdh6aN  42364  mapdh6dN  42368  mapdh6eN  42369  mapdh6hN  42372  mapdh7eN  42377  mapdh7dN  42379  mapdh7fN  42380  mapdh8ab  42406  mapdh8ad  42408  mapdh8e  42413  mapdh9a  42418  mapdh9aOLDN  42419  hdmap1l6a  42438  hdmap1l6d  42442  hdmap1l6e  42443  hdmap1l6h  42446  hdmap1eulem  42451  hdmap1eulemOLDN  42452  hdmapval0  42462  hdmapeveclem  42463  hdmapval3lemN  42466  hdmap10lem  42468  hdmap11lem1  42470  hdmaprnlem3N  42479  hdmaprnlem9N  42486  hdmaprnlem3eN  42487  fzne2d  42602  lcmineqlem11  42661  3lexlogpow5ineq1  42676  3lexlogpow5ineq2  42677  3lexlogpow5ineq4  42678  3lexlogpow5ineq3  42679  3lexlogpow2ineq1  42680  3lexlogpow2ineq2  42681  3lexlogpow5ineq5  42682  aks4d1lem1  42684  dvrelog2b  42688  dvrelogpow2b  42690  aks4d1p1p3  42691  aks4d1p1p2  42692  aks4d1p1p4  42693  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p1p5  42697  aks4d1p1  42698  aks4d1p2  42699  aks4d1p3  42700  aks4d1p5  42702  aks4d1p6  42703  aks4d1p7d1  42704  aks4d1p7  42705  aks4d1p8d3  42708  aks4d1p8  42709  aks4d1p9  42710  fldhmf1  42712  aks6d1c2p2  42741  hashscontpow  42744  aks6d1c3  42745  aks6d1c5lem2  42760  2np3bcnp1  42766  2ap1caineq  42767  sticksstones1  42768  sticksstones2  42769  sticksstones10  42777  sticksstones12a  42779  sticksstones12  42780  sticksstones22  42790  aks6d1c6lem4  42795  aks6d1c7lem2  42803  unitscyglem2  42818  unitscyglem4  42820  aks5lem8  42823  xppss12  42853  mhpind  43181  jm2.26lem3  43583  rpnnen3lem  43613  rpnnen3  43614  imo72b2lem2  44748  imo72b2  44753  mnuprdlem1  44839  bcc0  44907  chordthmALT  45499  fnchoice  45600  refsum2cnlem1  45608  xrleneltd  45890  xrltned  45924  infleinf  45938  reclt0  45957  icoiccdif  46091  ressiooinf  46124  limcresiooub  46207  limcleqr  46209  limclner  46216  climxrre  46315  icccncfext  46452  cncfiooiccre  46460  dvnxpaek  46507  stoweidlem43  46608  stirlinglem5  46643  stirlinglem7  46645  dirkercncflem1  46668  fourierdlem24  46696  fourierdlem32  46704  fourierdlem33  46705  fourierdlem34  46706  fourierdlem35  46707  fourierdlem46  46717  fourierdlem48  46719  fourierdlem49  46720  fourierdlem64  46735  fourierdlem65  46736  fourierdlem74  46745  fourierdlem76  46747  fourierdlem79  46750  fourierdlem81  46752  fourierdlem91  46762  fourierdlem102  46773  fourierdlem114  46785  etransclem15  46814  etransclem24  46823  sge0rpcpnf  46986  sge0isum  46992  pimrecltpos  47273  m1modne  47939  minusmod5ne  47940  m1modnep2mod  47943  modmknepk  47953  modm2nep1  47957  modm1nep2  47959  setsnidel  47974  odz2prm2pw  48163  fmtnoprmfac1lem  48164  fmtnoprmfac1  48165  fmtnoprmfac2  48167  lighneallem1  48205  lighneallem3  48207  perfectALTVlem2  48335  usgrgrtrirex  48563  isubgr3stgrlem6  48584  gpgusgralem  48669  gpg3nbgrvtx0  48689  pgnioedg1  48721  pgnioedg2  48722  pgnioedg5  48725  nnsgrpnmnd  48791  lvecpsslmod  49120  affinecomb1  49315  affinecomb2  49316  1subrec1sub  49318  rrx2plord2  49335  line  49345  rrxline  49347  eenglngeehlnmlem2  49351  rrx2vlinest  49354  line2xlem  49366  2itscp  49394