Theorem necomd 3011

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

Syntax hints:   → wi 4   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-ne 2957

This theorem is referenced by:  difsnb  4773  0nelop  5479  xpdifid  6165  f1ounsn  7270  resf1extb  7930  difsnen  9046  fofinf1o  9288  en2eleq  9991  en2other2  9992  ackbij1lem15  10215  infpssrlem5  10290  fin23lem24  10305  fin23lem31  10326  isf32lem9  10344  canthnumlem  10632  canthp1lem2  10637  npomex  10980  ltned  11345  lt0ne0  11679  recgt0  12060  zneo  12678  xrltne  13187  supxrbnd  13353  flltnz  13843  seqf1olem1  14076  nn0opthi  14305  hashtpg  14521  hash7g  14522  hashge3el3dif  14523  cats1un  14757  sumtp  15799  geoserg  15919  geolim  15923  geolim2  15924  tanadd  16222  ruclem6  16290  ruclem7  16291  isprm2lem  16738  isprm5  16765  oddprm  16869  pcmpt  16951  cshwshashlem3  17156  resshom  17470  ressco  17471  mrissmrcd  17695  rescco  17888  estrres  18194  chnccat  18681  chnrev  18682  chnpof1  18685  smndex2dnrinv  18976  pmtrprfv  19522  symggen  19539  dprdcntz  20079  dprdres  20099  ablfac1b  20141  01eq0ringOLD  20614  nrhmzr  20621  ornglmullt  20951  orngrmullt  20952  orngmullt  20953  ofldlt1  20957  lbspss  21182  lspsnnecom  21222  lspindp2l  21237  lspindp2  21238  islbs3  21258  lbsextlem4  21264  lidlnz  21355  isfieldidl  21365  qsidomlem2  21460  ssdifidlprm  21465  ofldchr  21705  uvcf1  21921  frlmup2  21928  psrridm  22091  coe1tmfv2  22415  coe1tmmul  22417  dmatmul  22633  mdetralt  22744  mdetunilem2  22749  mdetunilem6  22753  mdetunilem7  22754  maducoeval2  22776  madurid  22780  fvmptnn04ifa  22986  en2top  23121  cmpfi  23544  snfil  24000  tsmsfbas  24264  zcld  24950  iccpnfhmeo  25083  xrhmeo  25084  evth  25097  minveclem3b  25566  i1fres  25843  dvcnvlem  26114  ig1peu  26311  ig1pdvds  26316  aaliou3lem9  26490  taylthlem2  26513  abelthlem2  26571  abelthlem7  26577  cos02pilt1  26667  tanregt0  26680  logcj  26747  argimgt0  26753  dvloglem  26789  logf1o2  26791  logbrec  26923  ang180lem1  26950  ang180lem2  26951  ang180lem3  26952  ang180lem4  26953  ang180lem5  26954  ang180  26955  isosctrlem3  26961  ssscongptld  26963  affineequivne  26968  angpieqvdlem  26969  angpieqvdlem2  26970  angpieqvd  26972  chordthmlem  26973  chordthmlem2  26974  chordthm  26978  asinneg  27027  ppiltx  27317  perfectlem2  27370  lgsneg  27461  lgsqr  27491  lgseisenlem4  27518  lgsquadlem1  27520  lgsquadlem3  27522  lgsquad2  27526  2lgsoddprm  27556  dchrisum0flblem1  27648  noseponlem  27804  nosep1o  27821  nosep2o  27822  nosupbnd2lem1  27855  noinfbnd2lem1  27870  noetasuplem4  27876  noetainflem4  27880  lesrec  27968  0elright  28081  tgbtwnouttr  28742  tgifscgr  28753  tgcgrxfr  28763  tglngval  28796  tgfscgr  28813  tgbtwnconn1lem3  28819  tgbtwnconn3  28822  legtrid  28836  hltr  28858  hlbtwn  28859  btwnhl1  28860  btwnhl  28862  hlcgrex  28864  hlcgreulem  28865  lncom  28871  tgisline  28876  tglineeltr  28880  tglineelsb2  28881  tglinecom  28884  tglinethru  28885  ncolncol  28896  coltr  28897  coltr3  28898  tglnpt3  28903  tglnpt4  28904  symquadlem  28942  midexlem  28945  mirlni  28947  ragcol  28954  ragcgr  28962  perpneq  28969  footexALT  28973  footexlem1  28974  footexlem2  28975  foot  28977  footne  28978  colperpexlem3  28988  mideulem2  28990  opphllem  28991  midex  28993  opphllem1  29003  opphllem2  29004  opphllem3  29005  opphllem4  29006  opphllem5  29007  opphllem6  29008  outpasch  29012  hlpasch  29013  lnopp2hpgb  29020  colhp  29027  lnincplng  29040  plngrotlem1  29043  plngrotlem2  29044  plngrot  29046  lnssplnglem  29047  lnssplng  29048  lmieu  29067  hypcgrlem1  29082  hypcgrlem2  29083  lnperpex  29086  trgcopy  29088  trgcopyeulem  29089  iscgra1  29094  cgrane2  29097  cgrane3  29098  cgrane4  29099  cgracgr  29102  cgraid  29103  cgraswap  29104  cgrcgra  29105  cgracom  29106  cgratr  29107  flatcgra  29108  cgraswaplr  29109  cgracol  29112  dfcgra2  29114  sacgr  29115  oacgr  29116  acopy  29117  acopyeu  29118  ragcgra  29119  ragsupplcgra  29121  ragraghl  29122  perpeqlem  29123  perpeq  29124  leagne2  29140  leagne3  29141  cgrg3col4  29143  tgsas1  29144  tgsas2  29146  tgasa1  29148  dfprlng2  29170  dfprlng3  29171  perpprlng  29173  prlngex  29174  prlngmolem1  29175  prlngmolem2  29176  prlngmo2  29179  prlngmid2  29183  ttgcontlem1  29200  brbtwn2  29221  axlowdimlem15  29272  axlowdimlem16  29273  axcontlem8  29287  upgrex  29408  edglnl  29459  umgrvad2edg  29529  nbupgr  29660  nbumgrvtx  29662  nbgr2vtx1edg  29666  nbuhgr2vtx1edgb  29668  nbupgrres  29680  cplgr3v  29751  cusgrexilem2  29758  usgredgsscusgredg  29775  1hegrvtxdg1r  29824  1egrvtxdg1r  29826  1egrvtxdg0  29827  pthdadjvtx  30043  pthdlem2lem  30082  wspniunwspnon  30238  umgr2cwwk2dif  30381  3pthdlem1  30481  uhgr3cyclex  30499  upgr4cycl4dv4e  30502  frgr3v  30592  1to3vfriswmgr  30597  frgrwopreglem5a  30628  frgrwopreglem3  30631  frgrhash2wsp  30649  staddi  32564  unidifsnne  32848  ifnefals  32860  coprprop  33010  sgnval2  33046  pmtrcnel  33375  pmtrcnel2  33376  psgnfzto1stlem  33386  cycpmco2lem1  33412  cycpmco2  33419  cyc2fvx  33420  cyc3co2  33426  cycpmrn  33429  tocyccntz  33430  cyc3evpm  33436  cyc3genpmlem  33437  isarchiofld  33485  drngidlhash  33707  mxidlnzr  33716  drng0mxidl  33724  drngmxidl  33725  qsdrng  33745  dflringlem3  33752  dflring3  33753  dflring4  33754  rsprprmprmidl  33778  deg1prod  33839  vietadeg1  33934  ply1annnr  34059  constrrtll  34087  constrrtlc1  34088  constrrtcclem  34090  constrrtcc  34091  constrfin  34102  constrelextdg2  34103  cos9thpiminplylem3  34140  1smat1  34160  submateqlem1  34163  ordtconnlem1  34280  esumrnmpt2  34424  cntnevol  34584  signstfveq0a  34929  repr0  34964  reprlt  34972  reprinfz1  34975  morleylemrneab  35024  nelscottrankgt  35484  cusgredgex  35580  2cycl2d  35597  acycgr1v  35607  derangenlem  35629  subfacp1lem1  35637  subfacp1lem3  35640  subfacp1lem5  35642  fmlasucdisj  35857  dfrdg4  36409  ifscgr  36502  cgrxfr  36513  btwnconn1lem8  36552  btwnconn3  36561  segcon2  36563  broutsideof3  36584  outsideoftr  36587  outsideofeq  36588  outsideofeu  36589  lineunray  36605  lineelsb2  36606  linethru  36611  mh-inf3f1  37018  mh-inf3sn  37019  unbdqndv2lem2  37065  knoppndvlem1  37067  knoppndvlem2  37068  knoppndvlem7  37073  knoppndvlem14  37080  bj-bary1lem  37920  bj-bary1lem1  37921  bj-bary1  37922  finxpreclem2  38002  finxp1o  38004  finxpreclem6  38008  fin2solem  38223  poimirlem9  38246  poimirlem15  38252  poimirlem20  38257  poimirlem24  38261  poimirlem25  38262  poimirlem27  38264  itg2addnclem2  38289  ftc1cnnc  38309  heibor1lem  38426  maxidln0  38662  lshpnelb  39726  lsatssn0  39744  lsatcv0  39773  lsat0cv  39775  lsatexch1  39788  l1cvat  39797  atlen0  40052  cvlsupr2  40085  atcvrj2b  40174  2atlt  40181  atbtwn  40188  3noncolr2  40191  4noncolr3  40195  3dimlem3  40203  3dimlem3OLDN  40204  3dimlem4  40206  3dimlem4OLDN  40207  3dim2  40210  1cvratex  40215  1cvrat  40218  ps-1  40219  ps-2  40220  hlatexch4  40223  3atlem4  40228  3atlem6  40230  4atlem0ae  40336  4atlem0be  40337  dalemccnedd  40429  dalemrotps  40433  dalem21  40436  dalem23  40438  dalem27  40441  dalem41  40455  dalem44  40458  dalem54  40468  lnatexN  40521  lnjatN  40522  llnexchb2lem  40610  llnexchb2  40611  lhpn0  40746  lhpexle3lem  40753  lhpmatb  40773  4atexlemswapqr  40805  4atexlemc  40811  4atexlemnclw  40812  4atexlemcnd  40814  4atexlemex4  40815  4atexlemex6  40816  4atex  40818  trlat  40911  trlval4  40930  cdlemc5  40937  cdlemd4  40943  cdlemd7  40946  cdlemd9  40948  cdleme0e  40959  cdleme3b  40971  cdleme3c  40972  cdleme3e  40974  cdleme3h  40977  cdleme7aa  40984  cdleme7e  40989  cdleme7ga  40990  cdleme9  40995  cdleme11c  41003  cdleme11e  41005  cdleme11fN  41006  cdleme11h  41008  cdleme11j  41009  cdleme11k  41010  cdleme15b  41017  cdleme15c  41018  cdleme17c  41030  cdleme18b  41034  cdlemesner  41038  cdleme20zN  41043  cdleme19c  41047  cdleme19d  41048  cdleme19e  41049  cdleme20m  41065  cdleme21a  41067  cdleme21b  41068  cdleme21c  41069  cdleme22f2  41089  cdleme28b  41113  cdleme36a  41202  cdleme36m  41203  cdleme41sn4aw  41217  cdleme43bN  41232  cdleme43dN  41234  cdleme46f2g2  41235  cdleme46f2g1  41236  cdleme4gfv  41249  cdlemeg46nlpq  41259  cdlemeg46req  41271  cdlemeg46fgN  41276  cdlemf1  41303  cdlemg8b  41370  cdlemg9a  41374  cdlemg12g  41391  cdlemg12  41392  cdlemg13a  41393  cdlemg17pq  41414  cdlemg18a  41420  cdlemg18c  41422  cdlemg19a  41425  cdlemg19  41426  cdlemg21  41428  cdlemg31b0N  41436  cdlemg31b0a  41437  cdlemg31c  41441  cdlemg33b0  41443  cdlemg33c0  41444  trlcone  41470  cdlemg42  41471  cdlemg44a  41473  cdlemg46  41477  cdlemh1  41557  cdlemh2  41558  cdlemh  41559  cdlemj3  41565  cdlemk3  41575  cdlemki  41583  cdlemksv2  41589  cdlemk12  41592  cdlemk14  41596  cdlemk15  41597  cdlemk7u  41612  cdlemk11u  41613  cdlemk12u  41614  cdlemk21N  41615  cdlemk20  41616  cdlemk22  41635  cdlemk26-3  41648  cdlemk27-3  41649  cdlemk28-3  41650  cdlemkfid3N  41667  cdlemk11ta  41671  cdlemk47  41691  cdlemk54  41700  dia2dimlem1  41806  dochsat  42125  dochshpncl  42126  lclkrlem2b  42250  lcfrlem21  42305  baerlem5amN  42458  baerlem5bmN  42459  baerlem5abmN  42460  mapdindp4  42465  mapdheq2  42471  mapdheq2biN  42472  mapdh6aN  42477  mapdh6dN  42481  mapdh6eN  42482  mapdh6hN  42485  mapdh7eN  42490  mapdh7dN  42492  mapdh7fN  42493  mapdh8ab  42519  mapdh8ad  42521  mapdh8e  42526  mapdh9a  42531  mapdh9aOLDN  42532  hdmap1l6a  42551  hdmap1l6d  42555  hdmap1l6e  42556  hdmap1l6h  42559  hdmap1eulem  42564  hdmap1eulemOLDN  42565  hdmapval0  42575  hdmapeveclem  42576  hdmapval3lemN  42579  hdmap10lem  42581  hdmap11lem1  42583  hdmaprnlem3N  42592  hdmaprnlem9N  42599  hdmaprnlem3eN  42600  fzne2d  42715  lcmineqlem11  42774  3lexlogpow5ineq1  42789  3lexlogpow5ineq2  42790  3lexlogpow5ineq4  42791  3lexlogpow5ineq3  42792  3lexlogpow2ineq1  42793  3lexlogpow2ineq2  42794  3lexlogpow5ineq5  42795  aks4d1lem1  42797  dvrelog2b  42801  dvrelogpow2b  42803  aks4d1p1p3  42804  aks4d1p1p2  42805  aks4d1p1p4  42806  aks4d1p1p6  42808  aks4d1p1p7  42809  aks4d1p1p5  42810  aks4d1p1  42811  aks4d1p2  42812  aks4d1p3  42813  aks4d1p5  42815  aks4d1p6  42816  aks4d1p7d1  42817  aks4d1p7  42818  aks4d1p8d3  42821  aks4d1p8  42822  aks4d1p9  42823  fldhmf1  42825  aks6d1c2p2  42854  hashscontpow  42857  aks6d1c3  42858  aks6d1c5lem2  42873  2np3bcnp1  42879  2ap1caineq  42880  sticksstones1  42881  sticksstones2  42882  sticksstones10  42890  sticksstones12a  42892  sticksstones12  42893  sticksstones22  42903  aks6d1c6lem4  42908  aks6d1c7lem2  42916  unitscyglem2  42931  unitscyglem4  42933  aks5lem8  42936  xppss12  42968  mhpind  43296  jm2.26lem3  43698  rpnnen3lem  43728  rpnnen3  43729  imo72b2lem2  44863  imo72b2  44868  mnuprdlem1  44952  bcc0  45020  chordthmALT  45611  fnchoice  45719  refsum2cnlem1  45727  xrleneltd  46009  xrltned  46043  infleinf  46057  reclt0  46076  icoiccdif  46210  ressiooinf  46243  limcresiooub  46326  limcleqr  46328  limclner  46335  climxrre  46434  icccncfext  46571  cncfiooiccre  46579  dvnxpaek  46626  stoweidlem43  46727  stirlinglem5  46762  stirlinglem7  46764  dirkercncflem1  46787  fourierdlem24  46815  fourierdlem32  46823  fourierdlem33  46824  fourierdlem34  46825  fourierdlem35  46826  fourierdlem46  46836  fourierdlem48  46838  fourierdlem49  46839  fourierdlem64  46854  fourierdlem65  46855  fourierdlem74  46864  fourierdlem76  46866  fourierdlem79  46869  fourierdlem81  46871  fourierdlem91  46881  fourierdlem102  46892  fourierdlem114  46904  etransclem15  46933  etransclem24  46942  sge0rpcpnf  47105  sge0isum  47111  pimrecltpos  47392  m1modne  48058  minusmod5ne  48059  m1modnep2mod  48062  modmknepk  48072  modm2nep1  48076  modm1nep2  48078  setsnidel  48093  odz2prm2pw  48282  fmtnoprmfac1lem  48283  fmtnoprmfac1  48284  fmtnoprmfac2  48286  lighneallem1  48324  lighneallem3  48326  perfectALTVlem2  48454  usgrgrtrirex  48682  isubgr3stgrlem6  48703  gpgusgralem  48788  gpg3nbgrvtx0  48808  pgnioedg1  48840  pgnioedg2  48841  pgnioedg5  48844  nnsgrpnmnd  48910  smprngprmrng  49071  lvecpsslmod  49254  affinecomb1  49449  affinecomb2  49450  1subrec1sub  49452  rrx2plord2  49469  line  49479  rrxline  49481  eenglngeehlnmlem2  49485  rrx2vlinest  49488  line2xlem  49500  2itscp  49528