Theorem necomd 3042

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

Syntax hints:   → wi 4   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  difsnb  4699  0nelop  5351  xpdifid  5992  difsnen  8582  fofinf1o  8783  en2eleq  9419  en2other2  9420  ackbij1lem15  9645  infpssrlem5  9718  fin23lem24  9733  fin23lem31  9754  isf32lem9  9772  canthnumlem  10059  canthp1lem2  10064  npomex  10407  ltned  10765  lt0ne0  11095  recgt0  11475  zneo  12053  xrltne  12544  supxrbnd  12709  flltnz  13176  seqf1olem1  13405  nn0opthi  13626  hashtpg  13839  hashge3el3dif  13840  cats1un  14074  sumtp  15096  geoserg  15213  geolim  15218  geolim2  15219  tanadd  15512  ruclem6  15580  ruclem7  15581  isprm2lem  16015  isprm5  16041  oddprm  16137  pcmpt  16218  cshwshashlem3  16423  mrissmrcd  16903  estrres  17381  smndex2dnrinv  18072  pmtrprfv  18573  symggen  18590  dprdcntz  19123  dprdres  19143  ablfac1b  19185  lbspss  19847  lspsnnecom  19884  lspindp2l  19899  lspindp2  19900  islbs3  19920  lbsextlem4  19926  sralem  19942  lidlnz  19994  01eq0ring  20038  uvcf1  20481  frlmup2  20488  psrridm  20642  coe1tmfv2  20904  coe1tmmul  20906  dmatmul  21102  mdetralt  21213  mdetunilem2  21218  mdetunilem6  21222  mdetunilem7  21223  maducoeval2  21245  madurid  21249  fvmptnn04ifa  21455  en2top  21590  cmpfi  22013  snfil  22469  tsmsfbas  22733  zcld  23418  iccpnfhmeo  23550  xrhmeo  23551  evth  23564  minveclem3b  24032  i1fres  24309  dvcnvlem  24579  ig1peu  24772  ig1pdvds  24777  aaliou3lem9  24946  taylthlem2  24969  abelthlem2  25027  abelthlem7  25033  cos02pilt1  25118  tanregt0  25131  logcj  25197  argimgt0  25203  dvloglem  25239  logf1o2  25241  logbrec  25368  ang180lem1  25395  ang180lem2  25396  ang180lem3  25397  ang180lem4  25398  ang180lem5  25399  ang180  25400  isosctrlem3  25406  ssscongptld  25408  affineequivne  25413  angpieqvdlem  25414  angpieqvdlem2  25415  angpieqvd  25417  chordthmlem  25418  chordthmlem2  25419  chordthm  25423  asinneg  25472  ppiltx  25762  perfectlem2  25814  lgsneg  25905  lgsqr  25935  lgseisenlem4  25962  lgsquadlem1  25964  lgsquadlem3  25966  lgsquad2  25970  2lgsoddprm  26000  dchrisum0flblem1  26092  tgbtwnouttr  26291  tgifscgr  26302  tgcgrxfr  26312  tglngval  26345  tgfscgr  26362  tgbtwnconn1lem3  26368  tgbtwnconn3  26371  legtrid  26385  hltr  26404  hlbtwn  26405  btwnhl1  26406  btwnhl  26408  hlcgrex  26410  hlcgreulem  26411  lncom  26416  tgisline  26421  tglineeltr  26425  tglineelsb2  26426  tglinecom  26429  tglinethru  26430  ncolncol  26440  coltr  26441  coltr3  26442  symquadlem  26483  midexlem  26486  ragcol  26493  ragcgr  26501  perpneq  26508  footexALT  26512  footexlem1  26513  footexlem2  26514  foot  26516  footne  26517  colperpexlem3  26526  mideulem2  26528  opphllem  26529  midex  26531  opphllem1  26541  opphllem2  26542  opphllem3  26543  opphllem4  26544  opphllem5  26545  opphllem6  26546  outpasch  26549  hlpasch  26550  lnopp2hpgb  26557  colhp  26564  lmieu  26578  hypcgrlem1  26593  hypcgrlem2  26594  lnperpex  26597  trgcopy  26598  trgcopyeulem  26599  iscgra1  26604  cgrane2  26607  cgrane3  26608  cgrane4  26609  cgracgr  26612  cgraid  26613  cgraswap  26614  cgrcgra  26615  cgracom  26616  cgratr  26617  flatcgra  26618  cgraswaplr  26619  cgracol  26622  dfcgra2  26624  sacgr  26625  oacgr  26626  acopy  26627  acopyeu  26628  leagne2  26644  leagne3  26645  cgrg3col4  26647  tgsas1  26648  tgsas2  26650  tgasa1  26652  ttgcontlem1  26679  cchhllem  26681  brbtwn2  26699  axlowdimlem15  26750  axlowdimlem16  26751  axcontlem8  26765  upgrex  26885  edglnl  26936  umgrvad2edg  27003  nbupgr  27134  nbumgrvtx  27136  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  nbupgrres  27154  cplgr3v  27225  cusgrexilem2  27232  usgredgsscusgredg  27249  1hegrvtxdg1r  27298  1egrvtxdg1r  27300  1egrvtxdg0  27301  pthdadjvtx  27519  pthdlem2lem  27556  wspniunwspnon  27709  umgr2cwwk2dif  27849  3pthdlem1  27949  uhgr3cyclex  27967  upgr4cycl4dv4e  27970  frgr3v  28060  1to3vfriswmgr  28065  frgrwopreglem5a  28096  frgrwopreglem3  28099  frgrhash2wsp  28117  staddi  30029  unidifsnne  30308  coprprop  30459  pmtrcnel  30783  pmtrcnel2  30784  psgnfzto1stlem  30792  cycpmco2lem1  30818  cycpmco2  30825  cyc2fvx  30826  cyc3co2  30832  cycpmrn  30835  tocyccntz  30836  cyc3evpm  30842  cyc3genpmlem  30843  ornglmullt  30931  orngrmullt  30932  orngmullt  30933  ofldlt1  30937  ofldchr  30938  isarchiofld  30941  qsidomlem2  31037  mxidlnzr  31047  1smat1  31157  submateqlem1  31160  madjusmdetlem2  31181  ordtconnlem1  31277  esumrnmpt2  31437  cntnevol  31597  signstfveq0a  31956  repr0  31992  reprlt  32000  reprinfz1  32003  cusgredgex  32481  2cycl2d  32499  acycgr1v  32509  derangenlem  32531  subfacp1lem1  32539  subfacp1lem3  32542  subfacp1lem5  32544  fmlasucdisj  32759  noseponlem  33284  nosep1o  33299  nosupbnd2lem1  33328  noetalem3  33332  slerec  33390  dfrdg4  33525  ifscgr  33618  cgrxfr  33629  btwnconn1lem8  33668  btwnconn3  33677  segcon2  33679  broutsideof3  33700  outsideoftr  33703  outsideofeq  33704  outsideofeu  33705  lineunray  33721  lineelsb2  33722  linethru  33727  unbdqndv2lem2  33962  knoppndvlem1  33964  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem14  33977  bj-bary1lem  34724  bj-bary1lem1  34725  bj-bary1  34726  finxpreclem2  34807  finxp1o  34809  finxpreclem6  34813  fin2solem  35043  poimirlem9  35066  poimirlem15  35072  poimirlem20  35077  poimirlem24  35081  poimirlem25  35082  poimirlem27  35084  itg2addnclem2  35109  ftc1cnnc  35129  heibor1lem  35247  maxidln0  35483  lshpnelb  36280  lsatssn0  36298  lsatcv0  36327  lsat0cv  36329  lsatexch1  36342  l1cvat  36351  atlen0  36606  cvlsupr2  36639  atcvrj2b  36728  2atlt  36735  atbtwn  36742  3noncolr2  36745  4noncolr3  36749  3dimlem3  36757  3dimlem3OLDN  36758  3dimlem4  36760  3dimlem4OLDN  36761  3dim2  36764  1cvratex  36769  1cvrat  36772  ps-1  36773  ps-2  36774  hlatexch4  36777  3atlem4  36782  3atlem6  36784  4atlem0ae  36890  4atlem0be  36891  dalemccnedd  36983  dalemrotps  36987  dalem21  36990  dalem23  36992  dalem27  36995  dalem41  37009  dalem44  37012  dalem54  37022  lnatexN  37075  lnjatN  37076  llnexchb2lem  37164  llnexchb2  37165  lhpn0  37300  lhpexle3lem  37307  lhpmatb  37327  4atexlemswapqr  37359  4atexlemc  37365  4atexlemnclw  37366  4atexlemcnd  37368  4atexlemex4  37369  4atexlemex6  37370  4atex  37372  trlat  37465  trlval4  37484  cdlemc5  37491  cdlemd4  37497  cdlemd7  37500  cdlemd9  37502  cdleme0e  37513  cdleme3b  37525  cdleme3c  37526  cdleme3e  37528  cdleme3h  37531  cdleme7aa  37538  cdleme7e  37543  cdleme7ga  37544  cdleme9  37549  cdleme11c  37557  cdleme11e  37559  cdleme11fN  37560  cdleme11h  37562  cdleme11j  37563  cdleme11k  37564  cdleme15b  37571  cdleme15c  37572  cdleme17c  37584  cdleme18b  37588  cdlemesner  37592  cdleme20zN  37597  cdleme19c  37601  cdleme19d  37602  cdleme19e  37603  cdleme20m  37619  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme22f2  37643  cdleme28b  37667  cdleme36a  37756  cdleme36m  37757  cdleme41sn4aw  37771  cdleme43bN  37786  cdleme43dN  37788  cdleme46f2g2  37789  cdleme46f2g1  37790  cdleme4gfv  37803  cdlemeg46nlpq  37813  cdlemeg46req  37825  cdlemeg46fgN  37830  cdlemf1  37857  cdlemg8b  37924  cdlemg9a  37928  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg17pq  37968  cdlemg18a  37974  cdlemg18c  37976  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg31b0N  37990  cdlemg31b0a  37991  cdlemg31c  37995  cdlemg33b0  37997  cdlemg33c0  37998  trlcone  38024  cdlemg42  38025  cdlemg44a  38027  cdlemg46  38031  cdlemh1  38111  cdlemh2  38112  cdlemh  38113  cdlemj3  38119  cdlemk3  38129  cdlemki  38137  cdlemksv2  38143  cdlemk12  38146  cdlemk14  38150  cdlemk15  38151  cdlemk7u  38166  cdlemk11u  38167  cdlemk12u  38168  cdlemk21N  38169  cdlemk20  38170  cdlemk22  38189  cdlemk26-3  38202  cdlemk27-3  38203  cdlemk28-3  38204  cdlemkfid3N  38221  cdlemk11ta  38225  cdlemk47  38245  cdlemk54  38254  dia2dimlem1  38360  dochsat  38679  dochshpncl  38680  lclkrlem2b  38804  lcfrlem21  38859  baerlem5amN  39012  baerlem5bmN  39013  baerlem5abmN  39014  mapdindp4  39019  mapdheq2  39025  mapdheq2biN  39026  mapdh6aN  39031  mapdh6dN  39035  mapdh6eN  39036  mapdh6hN  39039  mapdh7eN  39044  mapdh7dN  39046  mapdh7fN  39047  mapdh8ab  39073  mapdh8ad  39075  mapdh8e  39080  mapdh9a  39085  mapdh9aOLDN  39086  hdmap1l6a  39105  hdmap1l6d  39109  hdmap1l6e  39110  hdmap1l6h  39113  hdmap1eulem  39118  hdmap1eulemOLDN  39119  hdmapval0  39129  hdmapeveclem  39130  hdmapval3lemN  39133  hdmap10lem  39135  hdmap11lem1  39137  hdmaprnlem3N  39146  hdmaprnlem9N  39153  hdmaprnlem3eN  39154  fzne2d  39268  lcmineqlem11  39327  2np3bcnp1  39348  2ap1caineq  39349  metakunt7  39356  metakunt12  39361  metakunt22  39371  xppss12  39409  jm2.26lem3  39942  rpnnen3lem  39972  rpnnen3  39973  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2  40878  mnuprdlem1  40980  bcc0  41044  chordthmALT  41639  fnchoice  41658  refsum2cnlem1  41666  xrleneltd  41955  xrltned  41989  infleinf  42004  reclt0  42027  icoiccdif  42161  ressiooinf  42194  limcresiooub  42284  limcleqr  42286  limclner  42293  climxrre  42392  icccncfext  42529  cncfiooiccre  42537  dvnxpaek  42584  stoweidlem43  42685  stirlinglem5  42720  stirlinglem7  42722  dirkercncflem1  42745  fourierdlem24  42773  fourierdlem32  42781  fourierdlem33  42782  fourierdlem34  42783  fourierdlem35  42784  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem64  42812  fourierdlem65  42813  fourierdlem74  42822  fourierdlem76  42824  fourierdlem79  42827  fourierdlem81  42829  fourierdlem91  42839  fourierdlem102  42850  fourierdlem114  42862  etransclem15  42891  etransclem24  42900  sge0rpcpnf  43060  sge0isum  43066  pimrecltpos  43344  pimiooltgt  43346  setsnidel  43894  odz2prm2pw  44080  fmtnoprmfac1lem  44081  fmtnoprmfac1  44082  fmtnoprmfac2  44084  lighneallem1  44123  lighneallem3  44125  perfectALTVlem2  44240  nnsgrpnmnd  44438  nrhmzr  44497  lvecpsslmod  44916  affinecomb1  45116  affinecomb2  45117  1subrec1sub  45119  rrx2plord2  45136  line  45146  rrxline  45148  eenglngeehlnmlem2  45152  rrx2vlinest  45155  line2xlem  45167  2itscp  45195