Theorem necomd 2985

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

Syntax hints:   → wi 4   ≠ wne 2930

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 2705

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

This theorem is referenced by:  difsnb  4759  0nelop  5441  xpdifid  6123  f1ounsn  7215  resf1extb  7873  difsnen  8982  fofinf1o  9226  en2eleq  9909  en2other2  9910  ackbij1lem15  10134  infpssrlem5  10208  fin23lem24  10223  fin23lem31  10244  isf32lem9  10262  canthnumlem  10549  canthp1lem2  10554  npomex  10897  ltned  11259  lt0ne0  11593  recgt0  11977  zneo  12566  xrltne  13072  supxrbnd  13237  flltnz  13725  seqf1olem1  13958  nn0opthi  14187  hashtpg  14402  hash7g  14403  hashge3el3dif  14404  cats1un  14638  sumtp  15666  geoserg  15783  geolim  15787  geolim2  15788  tanadd  16086  ruclem6  16154  ruclem7  16155  isprm2lem  16602  isprm5  16628  oddprm  16732  pcmpt  16814  cshwshashlem3  17019  resshom  17332  ressco  17333  mrissmrcd  17556  rescco  17749  estrres  18055  chnccat  18542  chnrev  18543  chnpof1  18546  smndex2dnrinv  18833  pmtrprfv  19375  symggen  19392  dprdcntz  19932  dprdres  19952  ablfac1b  19994  01eq0ringOLD  20456  nrhmzr  20462  ornglmullt  20794  orngrmullt  20795  orngmullt  20796  ofldlt1  20800  lbspss  21026  lspsnnecom  21066  lspindp2l  21081  lspindp2  21082  islbs3  21102  lbsextlem4  21108  lidlnz  21189  ofldchr  21523  uvcf1  21739  frlmup2  21746  psrridm  21910  coe1tmfv2  22199  coe1tmmul  22201  dmatmul  22422  mdetralt  22533  mdetunilem2  22538  mdetunilem6  22542  mdetunilem7  22543  maducoeval2  22565  madurid  22569  fvmptnn04ifa  22775  en2top  22910  cmpfi  23333  snfil  23789  tsmsfbas  24053  zcld  24739  iccpnfhmeo  24880  xrhmeo  24881  evth  24895  minveclem3b  25365  i1fres  25643  dvcnvlem  25917  ig1peu  26117  ig1pdvds  26122  aaliou3lem9  26295  taylthlem2  26319  taylthlem2OLD  26320  abelthlem2  26379  abelthlem7  26385  cos02pilt1  26472  tanregt0  26485  logcj  26552  argimgt0  26558  dvloglem  26594  logf1o2  26596  logbrec  26729  ang180lem1  26756  ang180lem2  26757  ang180lem3  26758  ang180lem4  26759  ang180lem5  26760  ang180  26761  isosctrlem3  26767  ssscongptld  26769  affineequivne  26774  angpieqvdlem  26775  angpieqvdlem2  26776  angpieqvd  26778  chordthmlem  26779  chordthmlem2  26780  chordthm  26784  asinneg  26833  ppiltx  27124  perfectlem2  27178  lgsneg  27269  lgsqr  27299  lgseisenlem4  27326  lgsquadlem1  27328  lgsquadlem3  27330  lgsquad2  27334  2lgsoddprm  27364  dchrisum0flblem1  27456  noseponlem  27613  nosep1o  27630  nosep2o  27631  nosupbnd2lem1  27664  noinfbnd2lem1  27679  noetasuplem4  27685  noetainflem4  27689  slerec  27770  0elright  27867  tgbtwnouttr  28485  tgifscgr  28496  tgcgrxfr  28506  tglngval  28539  tgfscgr  28556  tgbtwnconn1lem3  28562  tgbtwnconn3  28565  legtrid  28579  hltr  28598  hlbtwn  28599  btwnhl1  28600  btwnhl  28602  hlcgrex  28604  hlcgreulem  28605  lncom  28610  tgisline  28615  tglineeltr  28619  tglineelsb2  28620  tglinecom  28623  tglinethru  28624  ncolncol  28634  coltr  28635  coltr3  28636  symquadlem  28677  midexlem  28680  ragcol  28687  ragcgr  28695  perpneq  28702  footexALT  28706  footexlem1  28707  footexlem2  28708  foot  28710  footne  28711  colperpexlem3  28720  mideulem2  28722  opphllem  28723  midex  28725  opphllem1  28735  opphllem2  28736  opphllem3  28737  opphllem4  28738  opphllem5  28739  opphllem6  28740  outpasch  28743  hlpasch  28744  lnopp2hpgb  28751  colhp  28758  lmieu  28772  hypcgrlem1  28787  hypcgrlem2  28788  lnperpex  28791  trgcopy  28792  trgcopyeulem  28793  iscgra1  28798  cgrane2  28801  cgrane3  28802  cgrane4  28803  cgracgr  28806  cgraid  28807  cgraswap  28808  cgrcgra  28809  cgracom  28810  cgratr  28811  flatcgra  28812  cgraswaplr  28813  cgracol  28816  dfcgra2  28818  sacgr  28819  oacgr  28820  acopy  28821  acopyeu  28822  leagne2  28838  leagne3  28839  cgrg3col4  28841  tgsas1  28842  tgsas2  28844  tgasa1  28846  ttgcontlem1  28873  brbtwn2  28894  axlowdimlem15  28945  axlowdimlem16  28946  axcontlem8  28960  upgrex  29081  edglnl  29132  umgrvad2edg  29202  nbupgr  29333  nbumgrvtx  29335  nbgr2vtx1edg  29339  nbuhgr2vtx1edgb  29341  nbupgrres  29353  cplgr3v  29424  cusgrexilem2  29431  usgredgsscusgredg  29449  1hegrvtxdg1r  29498  1egrvtxdg1r  29500  1egrvtxdg0  29501  pthdadjvtx  29717  pthdlem2lem  29756  wspniunwspnon  29912  umgr2cwwk2dif  30055  3pthdlem1  30155  uhgr3cyclex  30173  upgr4cycl4dv4e  30176  frgr3v  30266  1to3vfriswmgr  30271  frgrwopreglem5a  30302  frgrwopreglem3  30305  frgrhash2wsp  30323  staddi  32237  unidifsnne  32527  ifnefals  32539  coprprop  32691  sgnval2  32729  pmtrcnel  33069  pmtrcnel2  33070  psgnfzto1stlem  33080  cycpmco2lem1  33106  cycpmco2  33113  cyc2fvx  33114  cyc3co2  33120  cycpmrn  33123  tocyccntz  33124  cyc3evpm  33130  cyc3genpmlem  33131  isarchiofld  33179  drngidlhash  33410  qsidomlem2  33429  ssdifidlprm  33434  mxidlnzr  33443  drng0mxidl  33452  drngmxidl  33453  qsdrng  33473  rsprprmprmidl  33498  ply1annnr  33727  constrrtll  33755  constrrtlc1  33756  constrrtcclem  33758  constrrtcc  33759  constrfin  33770  constrelextdg2  33771  cos9thpiminplylem3  33808  1smat1  33828  submateqlem1  33831  ordtconnlem1  33948  esumrnmpt2  34092  cntnevol  34252  signstfveq0a  34600  repr0  34635  reprlt  34643  reprinfz1  34646  cusgredgex  35177  2cycl2d  35194  acycgr1v  35204  derangenlem  35226  subfacp1lem1  35234  subfacp1lem3  35237  subfacp1lem5  35239  fmlasucdisj  35454  dfrdg4  36006  ifscgr  36099  cgrxfr  36110  btwnconn1lem8  36149  btwnconn3  36158  segcon2  36160  broutsideof3  36181  outsideoftr  36184  outsideofeq  36185  outsideofeu  36186  lineunray  36202  lineelsb2  36203  linethru  36208  unbdqndv2lem2  36565  knoppndvlem1  36567  knoppndvlem2  36568  knoppndvlem7  36573  knoppndvlem14  36580  bj-bary1lem  37365  bj-bary1lem1  37366  bj-bary1  37367  finxpreclem2  37445  finxp1o  37447  finxpreclem6  37451  fin2solem  37656  poimirlem9  37679  poimirlem15  37685  poimirlem20  37690  poimirlem24  37694  poimirlem25  37695  poimirlem27  37697  itg2addnclem2  37722  ftc1cnnc  37742  heibor1lem  37859  maxidln0  38095  lshpnelb  39093  lsatssn0  39111  lsatcv0  39140  lsat0cv  39142  lsatexch1  39155  l1cvat  39164  atlen0  39419  cvlsupr2  39452  atcvrj2b  39541  2atlt  39548  atbtwn  39555  3noncolr2  39558  4noncolr3  39562  3dimlem3  39570  3dimlem3OLDN  39571  3dimlem4  39573  3dimlem4OLDN  39574  3dim2  39577  1cvratex  39582  1cvrat  39585  ps-1  39586  ps-2  39587  hlatexch4  39590  3atlem4  39595  3atlem6  39597  4atlem0ae  39703  4atlem0be  39704  dalemccnedd  39796  dalemrotps  39800  dalem21  39803  dalem23  39805  dalem27  39808  dalem41  39822  dalem44  39825  dalem54  39835  lnatexN  39888  lnjatN  39889  llnexchb2lem  39977  llnexchb2  39978  lhpn0  40113  lhpexle3lem  40120  lhpmatb  40140  4atexlemswapqr  40172  4atexlemc  40178  4atexlemnclw  40179  4atexlemcnd  40181  4atexlemex4  40182  4atexlemex6  40183  4atex  40185  trlat  40278  trlval4  40297  cdlemc5  40304  cdlemd4  40310  cdlemd7  40313  cdlemd9  40315  cdleme0e  40326  cdleme3b  40338  cdleme3c  40339  cdleme3e  40341  cdleme3h  40344  cdleme7aa  40351  cdleme7e  40356  cdleme7ga  40357  cdleme9  40362  cdleme11c  40370  cdleme11e  40372  cdleme11fN  40373  cdleme11h  40375  cdleme11j  40376  cdleme11k  40377  cdleme15b  40384  cdleme15c  40385  cdleme17c  40397  cdleme18b  40401  cdlemesner  40405  cdleme20zN  40410  cdleme19c  40414  cdleme19d  40415  cdleme19e  40416  cdleme20m  40432  cdleme21a  40434  cdleme21b  40435  cdleme21c  40436  cdleme22f2  40456  cdleme28b  40480  cdleme36a  40569  cdleme36m  40570  cdleme41sn4aw  40584  cdleme43bN  40599  cdleme43dN  40601  cdleme46f2g2  40602  cdleme46f2g1  40603  cdleme4gfv  40616  cdlemeg46nlpq  40626  cdlemeg46req  40638  cdlemeg46fgN  40643  cdlemf1  40670  cdlemg8b  40737  cdlemg9a  40741  cdlemg12g  40758  cdlemg12  40759  cdlemg13a  40760  cdlemg17pq  40781  cdlemg18a  40787  cdlemg18c  40789  cdlemg19a  40792  cdlemg19  40793  cdlemg21  40795  cdlemg31b0N  40803  cdlemg31b0a  40804  cdlemg31c  40808  cdlemg33b0  40810  cdlemg33c0  40811  trlcone  40837  cdlemg42  40838  cdlemg44a  40840  cdlemg46  40844  cdlemh1  40924  cdlemh2  40925  cdlemh  40926  cdlemj3  40932  cdlemk3  40942  cdlemki  40950  cdlemksv2  40956  cdlemk12  40959  cdlemk14  40963  cdlemk15  40964  cdlemk7u  40979  cdlemk11u  40980  cdlemk12u  40981  cdlemk21N  40982  cdlemk20  40983  cdlemk22  41002  cdlemk26-3  41015  cdlemk27-3  41016  cdlemk28-3  41017  cdlemkfid3N  41034  cdlemk11ta  41038  cdlemk47  41058  cdlemk54  41067  dia2dimlem1  41173  dochsat  41492  dochshpncl  41493  lclkrlem2b  41617  lcfrlem21  41672  baerlem5amN  41825  baerlem5bmN  41826  baerlem5abmN  41827  mapdindp4  41832  mapdheq2  41838  mapdheq2biN  41839  mapdh6aN  41844  mapdh6dN  41848  mapdh6eN  41849  mapdh6hN  41852  mapdh7eN  41857  mapdh7dN  41859  mapdh7fN  41860  mapdh8ab  41886  mapdh8ad  41888  mapdh8e  41893  mapdh9a  41898  mapdh9aOLDN  41899  hdmap1l6a  41918  hdmap1l6d  41922  hdmap1l6e  41923  hdmap1l6h  41926  hdmap1eulem  41931  hdmap1eulemOLDN  41932  hdmapval0  41942  hdmapeveclem  41943  hdmapval3lemN  41946  hdmap10lem  41948  hdmap11lem1  41950  hdmaprnlem3N  41959  hdmaprnlem9N  41966  hdmaprnlem3eN  41967  fzne2d  42083  lcmineqlem11  42142  3lexlogpow5ineq1  42157  3lexlogpow5ineq2  42158  3lexlogpow5ineq4  42159  3lexlogpow5ineq3  42160  3lexlogpow2ineq1  42161  3lexlogpow2ineq2  42162  3lexlogpow5ineq5  42163  aks4d1lem1  42165  dvrelog2b  42169  dvrelogpow2b  42171  aks4d1p1p3  42172  aks4d1p1p2  42173  aks4d1p1p4  42174  aks4d1p1p6  42176  aks4d1p1p7  42177  aks4d1p1p5  42178  aks4d1p1  42179  aks4d1p2  42180  aks4d1p3  42181  aks4d1p5  42183  aks4d1p6  42184  aks4d1p7d1  42185  aks4d1p7  42186  aks4d1p8d3  42189  aks4d1p8  42190  aks4d1p9  42191  fldhmf1  42193  aks6d1c2p2  42222  hashscontpow  42225  aks6d1c3  42226  aks6d1c5lem2  42241  2np3bcnp1  42247  2ap1caineq  42248  sticksstones1  42249  sticksstones2  42250  sticksstones10  42258  sticksstones12a  42260  sticksstones12  42261  sticksstones22  42271  aks6d1c6lem4  42276  aks6d1c7lem2  42284  unitscyglem2  42299  unitscyglem4  42301  aks5lem8  42304  xppss12  42337  mhpind  42702  jm2.26lem3  43108  rpnnen3lem  43138  rpnnen3  43139  imo72b2lem2  44274  imo72b2  44279  mnuprdlem1  44379  bcc0  44447  chordthmALT  45039  fnchoice  45140  refsum2cnlem1  45148  xrleneltd  45436  xrltned  45470  infleinf  45484  reclt0  45503  icoiccdif  45638  ressiooinf  45671  limcresiooub  45754  limcleqr  45756  limclner  45763  climxrre  45862  icccncfext  45999  cncfiooiccre  46007  dvnxpaek  46054  stoweidlem43  46155  stirlinglem5  46190  stirlinglem7  46192  dirkercncflem1  46215  fourierdlem24  46243  fourierdlem32  46251  fourierdlem33  46252  fourierdlem34  46253  fourierdlem35  46254  fourierdlem46  46264  fourierdlem48  46266  fourierdlem49  46267  fourierdlem64  46282  fourierdlem65  46283  fourierdlem74  46292  fourierdlem76  46294  fourierdlem79  46297  fourierdlem81  46299  fourierdlem91  46309  fourierdlem102  46320  fourierdlem114  46332  etransclem15  46361  etransclem24  46370  sge0rpcpnf  46533  sge0isum  46539  pimrecltpos  46820  m1modne  47462  minusmod5ne  47463  m1modnep2mod  47466  modmknepk  47476  modm2nep1  47480  modm1nep2  47482  setsnidel  47491  odz2prm2pw  47677  fmtnoprmfac1lem  47678  fmtnoprmfac1  47679  fmtnoprmfac2  47681  lighneallem1  47719  lighneallem3  47721  perfectALTVlem2  47836  usgrgrtrirex  48064  isubgr3stgrlem6  48085  gpgusgralem  48170  gpg3nbgrvtx0  48190  pgnioedg1  48222  pgnioedg2  48223  pgnioedg5  48226  nnsgrpnmnd  48292  lvecpsslmod  48622  affinecomb1  48817  affinecomb2  48818  1subrec1sub  48820  rrx2plord2  48837  line  48847  rrxline  48849  eenglngeehlnmlem2  48853  rrx2vlinest  48856  line2xlem  48868  2itscp  48896