Theorem necomd 3002

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

Syntax hints:   → wi 4   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  difsnb  4831  0nelop  5515  xpdifid  6199  difsnen  9119  fofinf1o  9400  en2eleq  10077  en2other2  10078  ackbij1lem15  10302  infpssrlem5  10376  fin23lem24  10391  fin23lem31  10412  isf32lem9  10430  canthnumlem  10717  canthp1lem2  10722  npomex  11065  ltned  11426  lt0ne0  11756  recgt0  12140  zneo  12726  xrltne  13225  supxrbnd  13390  flltnz  13862  seqf1olem1  14092  nn0opthi  14319  hashtpg  14534  hash7g  14535  hashge3el3dif  14536  cats1un  14769  sumtp  15797  geoserg  15914  geolim  15918  geolim2  15919  tanadd  16215  ruclem6  16283  ruclem7  16284  isprm2lem  16728  isprm5  16754  oddprm  16857  pcmpt  16939  cshwshashlem3  17145  resshom  17478  ressco  17479  mrissmrcd  17698  rescco  17894  estrres  18208  smndex2dnrinv  18950  pmtrprfv  19495  symggen  19512  dprdcntz  20052  dprdres  20072  ablfac1b  20114  01eq0ringOLD  20557  nrhmzr  20563  lbspss  21104  lspsnnecom  21144  lspindp2l  21159  lspindp2  21160  islbs3  21180  lbsextlem4  21186  sralemOLD  21199  lidlnz  21275  uvcf1  21835  frlmup2  21842  psrridm  22006  coe1tmfv2  22299  coe1tmmul  22301  dmatmul  22524  mdetralt  22635  mdetunilem2  22640  mdetunilem6  22644  mdetunilem7  22645  maducoeval2  22667  madurid  22671  fvmptnn04ifa  22877  en2top  23013  cmpfi  23437  snfil  23893  tsmsfbas  24157  zcld  24854  iccpnfhmeo  24995  xrhmeo  24996  evth  25010  minveclem3b  25481  i1fres  25760  dvcnvlem  26034  ig1peu  26234  ig1pdvds  26239  aaliou3lem9  26410  taylthlem2  26434  taylthlem2OLD  26435  abelthlem2  26494  abelthlem7  26500  cos02pilt1  26586  tanregt0  26599  logcj  26666  argimgt0  26672  dvloglem  26708  logf1o2  26710  logbrec  26843  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  ang180lem4  26873  ang180lem5  26874  ang180  26875  isosctrlem3  26881  ssscongptld  26883  affineequivne  26888  angpieqvdlem  26889  angpieqvdlem2  26890  angpieqvd  26892  chordthmlem  26893  chordthmlem2  26894  chordthm  26898  asinneg  26947  ppiltx  27238  perfectlem2  27292  lgsneg  27383  lgsqr  27413  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem3  27444  lgsquad2  27448  2lgsoddprm  27478  dchrisum0flblem1  27570  noseponlem  27727  nosep1o  27744  nosep2o  27745  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  slerec  27882  0elright  27967  tgbtwnouttr  28523  tgifscgr  28534  tgcgrxfr  28544  tglngval  28577  tgfscgr  28594  tgbtwnconn1lem3  28600  tgbtwnconn3  28603  legtrid  28617  hltr  28636  hlbtwn  28637  btwnhl1  28638  btwnhl  28640  hlcgrex  28642  hlcgreulem  28643  lncom  28648  tgisline  28653  tglineeltr  28657  tglineelsb2  28658  tglinecom  28661  tglinethru  28662  ncolncol  28672  coltr  28673  coltr3  28674  symquadlem  28715  midexlem  28718  ragcol  28725  ragcgr  28733  perpneq  28740  footexALT  28744  footexlem1  28745  footexlem2  28746  foot  28748  footne  28749  colperpexlem3  28758  mideulem2  28760  opphllem  28761  midex  28763  opphllem1  28773  opphllem2  28774  opphllem3  28775  opphllem4  28776  opphllem5  28777  opphllem6  28778  outpasch  28781  hlpasch  28782  lnopp2hpgb  28789  colhp  28796  lmieu  28810  hypcgrlem1  28825  hypcgrlem2  28826  lnperpex  28829  trgcopy  28830  trgcopyeulem  28831  iscgra1  28836  cgrane2  28839  cgrane3  28840  cgrane4  28841  cgracgr  28844  cgraid  28845  cgraswap  28846  cgrcgra  28847  cgracom  28848  cgratr  28849  flatcgra  28850  cgraswaplr  28851  cgracol  28854  dfcgra2  28856  sacgr  28857  oacgr  28858  acopy  28859  acopyeu  28860  leagne2  28876  leagne3  28877  cgrg3col4  28879  tgsas1  28880  tgsas2  28882  tgasa1  28884  ttgcontlem1  28917  cchhllemOLD  28920  brbtwn2  28938  axlowdimlem15  28989  axlowdimlem16  28990  axcontlem8  29004  upgrex  29127  edglnl  29178  umgrvad2edg  29248  nbupgr  29379  nbumgrvtx  29381  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nbupgrres  29399  cplgr3v  29470  cusgrexilem2  29477  usgredgsscusgredg  29495  1hegrvtxdg1r  29544  1egrvtxdg1r  29546  1egrvtxdg0  29547  pthdadjvtx  29766  pthdlem2lem  29803  wspniunwspnon  29956  umgr2cwwk2dif  30096  3pthdlem1  30196  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  frgr3v  30307  1to3vfriswmgr  30312  frgrwopreglem5a  30343  frgrwopreglem3  30346  frgrhash2wsp  30364  staddi  32278  unidifsnne  32564  ifnefals  32571  coprprop  32711  pmtrcnel  33082  pmtrcnel2  33083  psgnfzto1stlem  33093  cycpmco2lem1  33119  cycpmco2  33126  cyc2fvx  33127  cyc3co2  33133  cycpmrn  33136  tocyccntz  33137  cyc3evpm  33143  cyc3genpmlem  33144  ornglmullt  33302  orngrmullt  33303  orngmullt  33304  ofldlt1  33308  ofldchr  33309  isarchiofld  33312  drngidlhash  33427  qsidomlem2  33446  ssdifidlprm  33451  mxidlnzr  33460  drng0mxidl  33469  drngmxidl  33470  qsdrng  33490  rsprprmprmidl  33515  ply1annnr  33696  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  constrfin  33736  constrelextdg2  33737  1smat1  33750  submateqlem1  33753  madjusmdetlem2  33774  ordtconnlem1  33870  esumrnmpt2  34032  cntnevol  34192  signstfveq0a  34553  repr0  34588  reprlt  34596  reprinfz1  34599  cusgredgex  35089  2cycl2d  35107  acycgr1v  35117  derangenlem  35139  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  fmlasucdisj  35367  dfrdg4  35915  ifscgr  36008  cgrxfr  36019  btwnconn1lem8  36058  btwnconn3  36067  segcon2  36069  broutsideof3  36090  outsideoftr  36093  outsideofeq  36094  outsideofeu  36095  lineunray  36111  lineelsb2  36112  linethru  36117  unbdqndv2lem2  36476  knoppndvlem1  36478  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem14  36491  bj-bary1lem  37276  bj-bary1lem1  37277  bj-bary1  37278  finxpreclem2  37356  finxp1o  37358  finxpreclem6  37362  fin2solem  37566  poimirlem9  37589  poimirlem15  37595  poimirlem20  37600  poimirlem24  37604  poimirlem25  37605  poimirlem27  37607  itg2addnclem2  37632  ftc1cnnc  37652  heibor1lem  37769  maxidln0  38005  lshpnelb  38940  lsatssn0  38958  lsatcv0  38987  lsat0cv  38989  lsatexch1  39002  l1cvat  39011  atlen0  39266  cvlsupr2  39299  atcvrj2b  39389  2atlt  39396  atbtwn  39403  3noncolr2  39406  4noncolr3  39410  3dimlem3  39418  3dimlem3OLDN  39419  3dimlem4  39421  3dimlem4OLDN  39422  3dim2  39425  1cvratex  39430  1cvrat  39433  ps-1  39434  ps-2  39435  hlatexch4  39438  3atlem4  39443  3atlem6  39445  4atlem0ae  39551  4atlem0be  39552  dalemccnedd  39644  dalemrotps  39648  dalem21  39651  dalem23  39653  dalem27  39656  dalem41  39670  dalem44  39673  dalem54  39683  lnatexN  39736  lnjatN  39737  llnexchb2lem  39825  llnexchb2  39826  lhpn0  39961  lhpexle3lem  39968  lhpmatb  39988  4atexlemswapqr  40020  4atexlemc  40026  4atexlemnclw  40027  4atexlemcnd  40029  4atexlemex4  40030  4atexlemex6  40031  4atex  40033  trlat  40126  trlval4  40145  cdlemc5  40152  cdlemd4  40158  cdlemd7  40161  cdlemd9  40163  cdleme0e  40174  cdleme3b  40186  cdleme3c  40187  cdleme3e  40189  cdleme3h  40192  cdleme7aa  40199  cdleme7e  40204  cdleme7ga  40205  cdleme9  40210  cdleme11c  40218  cdleme11e  40220  cdleme11fN  40221  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme15b  40232  cdleme15c  40233  cdleme17c  40245  cdleme18b  40249  cdlemesner  40253  cdleme20zN  40258  cdleme19c  40262  cdleme19d  40263  cdleme19e  40264  cdleme20m  40280  cdleme21a  40282  cdleme21b  40283  cdleme21c  40284  cdleme22f2  40304  cdleme28b  40328  cdleme36a  40417  cdleme36m  40418  cdleme41sn4aw  40432  cdleme43bN  40447  cdleme43dN  40449  cdleme46f2g2  40450  cdleme46f2g1  40451  cdleme4gfv  40464  cdlemeg46nlpq  40474  cdlemeg46req  40486  cdlemeg46fgN  40491  cdlemf1  40518  cdlemg8b  40585  cdlemg9a  40589  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg17pq  40629  cdlemg18a  40635  cdlemg18c  40637  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg31b0N  40651  cdlemg31b0a  40652  cdlemg31c  40656  cdlemg33b0  40658  cdlemg33c0  40659  trlcone  40685  cdlemg42  40686  cdlemg44a  40688  cdlemg46  40692  cdlemh1  40772  cdlemh2  40773  cdlemh  40774  cdlemj3  40780  cdlemk3  40790  cdlemki  40798  cdlemksv2  40804  cdlemk12  40807  cdlemk14  40811  cdlemk15  40812  cdlemk7u  40827  cdlemk11u  40828  cdlemk12u  40829  cdlemk21N  40830  cdlemk20  40831  cdlemk22  40850  cdlemk26-3  40863  cdlemk27-3  40864  cdlemk28-3  40865  cdlemkfid3N  40882  cdlemk11ta  40886  cdlemk47  40906  cdlemk54  40915  dia2dimlem1  41021  dochsat  41340  dochshpncl  41341  lclkrlem2b  41465  lcfrlem21  41520  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdindp4  41680  mapdheq2  41686  mapdheq2biN  41687  mapdh6aN  41692  mapdh6dN  41696  mapdh6eN  41697  mapdh6hN  41700  mapdh7eN  41705  mapdh7dN  41707  mapdh7fN  41708  mapdh8ab  41734  mapdh8ad  41736  mapdh8e  41741  mapdh9a  41746  mapdh9aOLDN  41747  hdmap1l6a  41766  hdmap1l6d  41770  hdmap1l6e  41771  hdmap1l6h  41774  hdmap1eulem  41779  hdmap1eulemOLDN  41780  hdmapval0  41790  hdmapeveclem  41791  hdmapval3lemN  41794  hdmap10lem  41796  hdmap11lem1  41798  hdmaprnlem3N  41807  hdmaprnlem9N  41814  hdmaprnlem3eN  41815  fzne2d  41937  lcmineqlem11  41996  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1lem1  42019  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  fldhmf1  42047  aks6d1c2p2  42076  hashscontpow  42079  aks6d1c3  42080  aks6d1c5lem2  42095  2np3bcnp1  42101  2ap1caineq  42102  sticksstones1  42103  sticksstones2  42104  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem4  42130  aks6d1c7lem2  42138  unitscyglem2  42153  unitscyglem4  42155  aks5lem8  42158  metakunt7  42168  metakunt12  42173  metakunt22  42183  xppss12  42222  mhpind  42549  jm2.26lem3  42958  rpnnen3lem  42988  rpnnen3  42989  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2  44134  mnuprdlem1  44241  bcc0  44309  chordthmALT  44904  fnchoice  44929  refsum2cnlem1  44937  xrleneltd  45238  xrltned  45272  infleinf  45287  reclt0  45306  icoiccdif  45442  ressiooinf  45475  limcresiooub  45563  limcleqr  45565  limclner  45572  climxrre  45671  icccncfext  45808  cncfiooiccre  45816  dvnxpaek  45863  stoweidlem43  45964  stirlinglem5  45999  stirlinglem7  46001  dirkercncflem1  46024  fourierdlem24  46052  fourierdlem32  46060  fourierdlem33  46061  fourierdlem34  46062  fourierdlem35  46063  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem64  46091  fourierdlem65  46092  fourierdlem74  46101  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem91  46118  fourierdlem102  46129  fourierdlem114  46141  etransclem15  46170  etransclem24  46179  sge0rpcpnf  46342  sge0isum  46348  pimrecltpos  46629  pimiooltgt  46631  setsnidel  47251  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  fmtnoprmfac2  47441  lighneallem1  47479  lighneallem3  47481  perfectALTVlem2  47596  usgrgrtrirex  47799  nnsgrpnmnd  47901  lvecpsslmod  48236  affinecomb1  48436  affinecomb2  48437  1subrec1sub  48439  rrx2plord2  48456  line  48466  rrxline  48468  eenglngeehlnmlem2  48472  rrx2vlinest  48475  line2xlem  48487  2itscp  48515