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 217	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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-ne 2933

This theorem is referenced by:  difsnb  4802  0nelop  5487  xpdifid  6158  difsnen  9050  fofinf1o  9324  en2eleq  10000  en2other2  10001  ackbij1lem15  10226  infpssrlem5  10299  fin23lem24  10314  fin23lem31  10335  isf32lem9  10353  canthnumlem  10640  canthp1lem2  10645  npomex  10988  ltned  11349  lt0ne0  11679  recgt0  12059  zneo  12644  xrltne  13143  supxrbnd  13308  flltnz  13777  seqf1olem1  14008  nn0opthi  14231  hashtpg  14448  hashge3el3dif  14449  cats1un  14673  sumtp  15697  geoserg  15814  geolim  15818  geolim2  15819  tanadd  16113  ruclem6  16181  ruclem7  16182  isprm2lem  16621  isprm5  16647  oddprm  16748  pcmpt  16830  cshwshashlem3  17036  resshom  17369  ressco  17370  mrissmrcd  17589  rescco  17785  estrres  18099  smndex2dnrinv  18836  pmtrprfv  19369  symggen  19386  dprdcntz  19926  dprdres  19946  ablfac1b  19988  01eq0ringOLD  20427  nrhmzr  20433  lbspss  20926  lspsnnecom  20966  lspindp2l  20981  lspindp2  20982  islbs3  21002  lbsextlem4  21008  sralemOLD  21021  lidlnz  21096  uvcf1  21676  frlmup2  21683  psrridm  21855  coe1tmfv2  22138  coe1tmmul  22140  dmatmul  22343  mdetralt  22454  mdetunilem2  22459  mdetunilem6  22463  mdetunilem7  22464  maducoeval2  22486  madurid  22490  fvmptnn04ifa  22696  en2top  22832  cmpfi  23256  snfil  23712  tsmsfbas  23976  zcld  24673  iccpnfhmeo  24814  xrhmeo  24815  evth  24829  minveclem3b  25300  i1fres  25579  dvcnvlem  25852  ig1peu  26052  ig1pdvds  26057  aaliou3lem9  26227  taylthlem2  26250  abelthlem2  26309  abelthlem7  26315  cos02pilt1  26400  tanregt0  26413  logcj  26480  argimgt0  26486  dvloglem  26522  logf1o2  26524  logbrec  26654  ang180lem1  26681  ang180lem2  26682  ang180lem3  26683  ang180lem4  26684  ang180lem5  26685  ang180  26686  isosctrlem3  26692  ssscongptld  26694  affineequivne  26699  angpieqvdlem  26700  angpieqvdlem2  26701  angpieqvd  26703  chordthmlem  26704  chordthmlem2  26705  chordthm  26709  asinneg  26758  ppiltx  27049  perfectlem2  27103  lgsneg  27194  lgsqr  27224  lgseisenlem4  27251  lgsquadlem1  27253  lgsquadlem3  27255  lgsquad2  27259  2lgsoddprm  27289  dchrisum0flblem1  27381  noseponlem  27537  nosep1o  27554  nosep2o  27555  nosupbnd2lem1  27588  noinfbnd2lem1  27603  noetasuplem4  27609  noetainflem4  27613  slerec  27692  0elright  27777  tgbtwnouttr  28241  tgifscgr  28252  tgcgrxfr  28262  tglngval  28295  tgfscgr  28312  tgbtwnconn1lem3  28318  tgbtwnconn3  28321  legtrid  28335  hltr  28354  hlbtwn  28355  btwnhl1  28356  btwnhl  28358  hlcgrex  28360  hlcgreulem  28361  lncom  28366  tgisline  28371  tglineeltr  28375  tglineelsb2  28376  tglinecom  28379  tglinethru  28380  ncolncol  28390  coltr  28391  coltr3  28392  symquadlem  28433  midexlem  28436  ragcol  28443  ragcgr  28451  perpneq  28458  footexALT  28462  footexlem1  28463  footexlem2  28464  foot  28466  footne  28467  colperpexlem3  28476  mideulem2  28478  opphllem  28479  midex  28481  opphllem1  28491  opphllem2  28492  opphllem3  28493  opphllem4  28494  opphllem5  28495  opphllem6  28496  outpasch  28499  hlpasch  28500  lnopp2hpgb  28507  colhp  28514  lmieu  28528  hypcgrlem1  28543  hypcgrlem2  28544  lnperpex  28547  trgcopy  28548  trgcopyeulem  28549  iscgra1  28554  cgrane2  28557  cgrane3  28558  cgrane4  28559  cgracgr  28562  cgraid  28563  cgraswap  28564  cgrcgra  28565  cgracom  28566  cgratr  28567  flatcgra  28568  cgraswaplr  28569  cgracol  28572  dfcgra2  28574  sacgr  28575  oacgr  28576  acopy  28577  acopyeu  28578  leagne2  28594  leagne3  28595  cgrg3col4  28597  tgsas1  28598  tgsas2  28600  tgasa1  28602  ttgcontlem1  28635  cchhllemOLD  28638  brbtwn2  28656  axlowdimlem15  28707  axlowdimlem16  28708  axcontlem8  28722  upgrex  28845  edglnl  28896  umgrvad2edg  28963  nbupgr  29094  nbumgrvtx  29096  nbgr2vtx1edg  29100  nbuhgr2vtx1edgb  29102  nbupgrres  29114  cplgr3v  29185  cusgrexilem2  29192  usgredgsscusgredg  29210  1hegrvtxdg1r  29259  1egrvtxdg1r  29261  1egrvtxdg0  29262  pthdadjvtx  29481  pthdlem2lem  29518  wspniunwspnon  29671  umgr2cwwk2dif  29811  3pthdlem1  29911  uhgr3cyclex  29929  upgr4cycl4dv4e  29932  frgr3v  30022  1to3vfriswmgr  30027  frgrwopreglem5a  30058  frgrwopreglem3  30061  frgrhash2wsp  30079  staddi  31993  unidifsnne  32267  ifnefals  32274  coprprop  32415  pmtrcnel  32743  pmtrcnel2  32744  psgnfzto1stlem  32752  cycpmco2lem1  32778  cycpmco2  32785  cyc2fvx  32786  cyc3co2  32792  cycpmrn  32795  tocyccntz  32796  cyc3evpm  32802  cyc3genpmlem  32803  ornglmullt  32917  orngrmullt  32918  orngmullt  32919  ofldlt1  32923  ofldchr  32924  isarchiofld  32927  drngidlhash  33047  qsidomlem2  33067  mxidlnzr  33078  drng0mxidl  33087  drngmxidl  33088  qsdrng  33106  ply1annnr  33272  1smat1  33303  submateqlem1  33306  madjusmdetlem2  33327  ordtconnlem1  33423  esumrnmpt2  33585  cntnevol  33745  signstfveq0a  34106  repr0  34141  reprlt  34149  reprinfz1  34152  cusgredgex  34629  2cycl2d  34647  acycgr1v  34657  derangenlem  34679  subfacp1lem1  34687  subfacp1lem3  34690  subfacp1lem5  34692  fmlasucdisj  34907  dfrdg4  35445  ifscgr  35538  cgrxfr  35549  btwnconn1lem8  35588  btwnconn3  35597  segcon2  35599  broutsideof3  35620  outsideoftr  35623  outsideofeq  35624  outsideofeu  35625  lineunray  35641  lineelsb2  35642  linethru  35647  gg-taylthlem2  35683  unbdqndv2lem2  35886  knoppndvlem1  35888  knoppndvlem2  35889  knoppndvlem7  35894  knoppndvlem14  35901  bj-bary1lem  36691  bj-bary1lem1  36692  bj-bary1  36693  finxpreclem2  36771  finxp1o  36773  finxpreclem6  36777  fin2solem  36977  poimirlem9  37000  poimirlem15  37006  poimirlem20  37011  poimirlem24  37015  poimirlem25  37016  poimirlem27  37018  itg2addnclem2  37043  ftc1cnnc  37063  heibor1lem  37180  maxidln0  37416  lshpnelb  38357  lsatssn0  38375  lsatcv0  38404  lsat0cv  38406  lsatexch1  38419  l1cvat  38428  atlen0  38683  cvlsupr2  38716  atcvrj2b  38806  2atlt  38813  atbtwn  38820  3noncolr2  38823  4noncolr3  38827  3dimlem3  38835  3dimlem3OLDN  38836  3dimlem4  38838  3dimlem4OLDN  38839  3dim2  38842  1cvratex  38847  1cvrat  38850  ps-1  38851  ps-2  38852  hlatexch4  38855  3atlem4  38860  3atlem6  38862  4atlem0ae  38968  4atlem0be  38969  dalemccnedd  39061  dalemrotps  39065  dalem21  39068  dalem23  39070  dalem27  39073  dalem41  39087  dalem44  39090  dalem54  39100  lnatexN  39153  lnjatN  39154  llnexchb2lem  39242  llnexchb2  39243  lhpn0  39378  lhpexle3lem  39385  lhpmatb  39405  4atexlemswapqr  39437  4atexlemc  39443  4atexlemnclw  39444  4atexlemcnd  39446  4atexlemex4  39447  4atexlemex6  39448  4atex  39450  trlat  39543  trlval4  39562  cdlemc5  39569  cdlemd4  39575  cdlemd7  39578  cdlemd9  39580  cdleme0e  39591  cdleme3b  39603  cdleme3c  39604  cdleme3e  39606  cdleme3h  39609  cdleme7aa  39616  cdleme7e  39621  cdleme7ga  39622  cdleme9  39627  cdleme11c  39635  cdleme11e  39637  cdleme11fN  39638  cdleme11h  39640  cdleme11j  39641  cdleme11k  39642  cdleme15b  39649  cdleme15c  39650  cdleme17c  39662  cdleme18b  39666  cdlemesner  39670  cdleme20zN  39675  cdleme19c  39679  cdleme19d  39680  cdleme19e  39681  cdleme20m  39697  cdleme21a  39699  cdleme21b  39700  cdleme21c  39701  cdleme22f2  39721  cdleme28b  39745  cdleme36a  39834  cdleme36m  39835  cdleme41sn4aw  39849  cdleme43bN  39864  cdleme43dN  39866  cdleme46f2g2  39867  cdleme46f2g1  39868  cdleme4gfv  39881  cdlemeg46nlpq  39891  cdlemeg46req  39903  cdlemeg46fgN  39908  cdlemf1  39935  cdlemg8b  40002  cdlemg9a  40006  cdlemg12g  40023  cdlemg12  40024  cdlemg13a  40025  cdlemg17pq  40046  cdlemg18a  40052  cdlemg18c  40054  cdlemg19a  40057  cdlemg19  40058  cdlemg21  40060  cdlemg31b0N  40068  cdlemg31b0a  40069  cdlemg31c  40073  cdlemg33b0  40075  cdlemg33c0  40076  trlcone  40102  cdlemg42  40103  cdlemg44a  40105  cdlemg46  40109  cdlemh1  40189  cdlemh2  40190  cdlemh  40191  cdlemj3  40197  cdlemk3  40207  cdlemki  40215  cdlemksv2  40221  cdlemk12  40224  cdlemk14  40228  cdlemk15  40229  cdlemk7u  40244  cdlemk11u  40245  cdlemk12u  40246  cdlemk21N  40247  cdlemk20  40248  cdlemk22  40267  cdlemk26-3  40280  cdlemk27-3  40281  cdlemk28-3  40282  cdlemkfid3N  40299  cdlemk11ta  40303  cdlemk47  40323  cdlemk54  40332  dia2dimlem1  40438  dochsat  40757  dochshpncl  40758  lclkrlem2b  40882  lcfrlem21  40937  baerlem5amN  41090  baerlem5bmN  41091  baerlem5abmN  41092  mapdindp4  41097  mapdheq2  41103  mapdheq2biN  41104  mapdh6aN  41109  mapdh6dN  41113  mapdh6eN  41114  mapdh6hN  41117  mapdh7eN  41122  mapdh7dN  41124  mapdh7fN  41125  mapdh8ab  41151  mapdh8ad  41153  mapdh8e  41158  mapdh9a  41163  mapdh9aOLDN  41164  hdmap1l6a  41183  hdmap1l6d  41187  hdmap1l6e  41188  hdmap1l6h  41191  hdmap1eulem  41196  hdmap1eulemOLDN  41197  hdmapval0  41207  hdmapeveclem  41208  hdmapval3lemN  41211  hdmap10lem  41213  hdmap11lem1  41215  hdmaprnlem3N  41224  hdmaprnlem9N  41231  hdmaprnlem3eN  41232  fzne2d  41352  lcmineqlem11  41410  3lexlogpow5ineq1  41425  3lexlogpow5ineq2  41426  3lexlogpow5ineq4  41427  3lexlogpow5ineq3  41428  3lexlogpow2ineq1  41429  3lexlogpow2ineq2  41430  3lexlogpow5ineq5  41431  aks4d1lem1  41433  dvrelog2b  41437  dvrelogpow2b  41439  aks4d1p1p3  41440  aks4d1p1p2  41441  aks4d1p1p4  41442  aks4d1p1p6  41444  aks4d1p1p7  41445  aks4d1p1p5  41446  aks4d1p1  41447  aks4d1p2  41448  aks4d1p3  41449  aks4d1p5  41451  aks4d1p6  41452  aks4d1p7d1  41453  aks4d1p7  41454  aks4d1p8d3  41457  aks4d1p8  41458  aks4d1p9  41459  fldhmf1  41461  aks6d1c2p2  41486  hashscontpow  41489  aks6d1c3  41490  2np3bcnp1  41493  2ap1caineq  41494  sticksstones1  41495  sticksstones2  41496  sticksstones10  41504  sticksstones12a  41506  sticksstones12  41507  sticksstones22  41517  metakunt7  41524  metakunt12  41529  metakunt22  41539  xppss12  41580  mhpind  41695  jm2.26lem3  42290  rpnnen3lem  42320  rpnnen3  42321  imo72b2lem0  43466  imo72b2lem2  43468  imo72b2  43473  mnuprdlem1  43580  bcc0  43648  chordthmALT  44243  fnchoice  44262  refsum2cnlem1  44270  xrleneltd  44578  xrltned  44612  infleinf  44627  reclt0  44646  icoiccdif  44782  ressiooinf  44815  limcresiooub  44903  limcleqr  44905  limclner  44912  climxrre  45011  icccncfext  45148  cncfiooiccre  45156  dvnxpaek  45203  stoweidlem43  45304  stirlinglem5  45339  stirlinglem7  45341  dirkercncflem1  45364  fourierdlem24  45392  fourierdlem32  45400  fourierdlem33  45401  fourierdlem34  45402  fourierdlem35  45403  fourierdlem46  45413  fourierdlem48  45415  fourierdlem49  45416  fourierdlem64  45431  fourierdlem65  45432  fourierdlem74  45441  fourierdlem76  45443  fourierdlem79  45446  fourierdlem81  45448  fourierdlem91  45458  fourierdlem102  45469  fourierdlem114  45481  etransclem15  45510  etransclem24  45519  sge0rpcpnf  45682  sge0isum  45688  pimrecltpos  45969  pimiooltgt  45971  setsnidel  46590  odz2prm2pw  46776  fmtnoprmfac1lem  46777  fmtnoprmfac1  46778  fmtnoprmfac2  46780  lighneallem1  46818  lighneallem3  46820  perfectALTVlem2  46935  nnsgrpnmnd  47101  lvecpsslmod  47436  affinecomb1  47636  affinecomb2  47637  1subrec1sub  47639  rrx2plord2  47656  line  47666  rrxline  47668  eenglngeehlnmlem2  47672  rrx2vlinest  47675  line2xlem  47687  2itscp  47715