Theorem necomd 2849

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

Syntax hints:   → wi 4   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  difsnb  4337  0nelop  4960  xpdifid  5562  difsnen  8042  fofinf1o  8241  en2eleq  8831  en2other2  8832  ackbij1lem15  9056  infpssrlem5  9129  fin23lem24  9144  fin23lem31  9165  isf32lem9  9183  canthnumlem  9470  canthp1lem2  9475  npomex  9818  ltned  10173  lt0ne0  10494  recgt0  10867  zneo  11460  xrltne  11994  supxrbnd  12158  flltnz  12612  seqf1olem1  12840  nn0opthi  13057  hashtpg  13267  hashge3el3dif  13268  cats1un  13475  sumtp  14478  geoserg  14598  geolim  14601  geolim2  14602  tanadd  14897  ruclem6  14964  ruclem7  14965  isprm2lem  15394  isprm5  15419  oddprm  15515  pcmpt  15596  cshwshashlem3  15804  mrissmrcd  16300  estrres  16779  pmtrprfv  17873  symggen  17890  dprdcntz  18407  dprdres  18427  ablfac1b  18469  lbspss  19082  lspsnnecom  19119  lspindp2l  19134  lspindp2  19135  islbs3  19155  lbsextlem4  19161  sralem  19177  lidlnz  19228  01eq0ring  19272  psrridm  19404  coe1tmfv2  19645  coe1tmmul  19647  uvcf1  20131  frlmup2  20138  dmatmul  20303  mdetralt  20414  mdetunilem2  20419  mdetunilem6  20423  mdetunilem7  20424  maducoeval2  20446  madurid  20450  fvmptnn04ifa  20655  en2top  20789  cmpfi  21211  snfil  21668  tsmsfbas  21931  zcld  22616  iccpnfhmeo  22744  xrhmeo  22745  evth  22758  minveclem3b  23199  i1fres  23472  dvcnvlem  23739  ig1peu  23931  ig1pdvds  23936  aaliou3lem9  24105  taylthlem2  24128  abelthlem2  24186  abelthlem7  24192  tanregt0  24285  logcj  24352  argimgt0  24358  dvloglem  24394  logf1o2  24396  logbrec  24520  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  ang180lem4  24542  ang180lem5  24543  ang180  24544  isosctrlem3  24550  ssscongptld  24552  angpieqvdlem  24555  angpieqvdlem2  24556  angpieqvd  24558  chordthmlem  24559  chordthmlem2  24560  chordthm  24564  asinneg  24613  ppiltx  24903  perfectlem2  24955  lgsneg  25046  lgsqr  25076  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem3  25107  lgsquad2  25111  2lgsoddprm  25141  dchrisum0flblem1  25197  tgbtwnouttr  25392  tgifscgr  25403  tgcgrxfr  25413  tglngval  25446  tgfscgr  25463  tgbtwnconn1lem3  25469  tgbtwnconn3  25472  legtrid  25486  hltr  25505  hlbtwn  25506  btwnhl1  25507  btwnhl  25509  hlcgrex  25511  hlcgreulem  25512  lncom  25517  tgisline  25522  tglineeltr  25526  tglineelsb2  25527  tglinecom  25530  tglinethru  25531  ncolncol  25541  coltr  25542  coltr3  25543  symquadlem  25584  midexlem  25587  ragcol  25594  ragcgr  25602  perpneq  25609  footex  25613  foot  25614  footne  25615  colperpexlem3  25624  mideulem2  25626  opphllem  25627  midex  25629  opphllem1  25639  opphllem2  25640  opphllem3  25641  opphllem4  25642  opphllem5  25643  opphllem6  25644  outpasch  25647  hlpasch  25648  lnopp2hpgb  25655  colhp  25662  lmieu  25676  hypcgrlem1  25691  hypcgrlem2  25692  lnperpex  25695  trgcopy  25696  trgcopyeulem  25697  iscgra1  25702  cgrane2  25705  cgrane3  25706  cgrane4  25707  cgracgr  25710  cgraid  25711  cgraswap  25712  cgrcgra  25713  cgracom  25714  cgratr  25715  cgraswaplr  25716  cgracol  25719  dfcgra2  25721  sacgr  25722  oacgr  25723  acopy  25724  acopyeu  25725  cgrg3col4  25734  tgsas1  25735  tgsas2  25737  tgasa1  25739  tgsss1  25741  isoas  25744  ttgcontlem1  25765  cchhllem  25767  brbtwn2  25785  axlowdimlem15  25836  axlowdimlem16  25837  axcontlem8  25851  upgrex  25987  edglnl  26038  umgrvad2edg  26105  nbupgr  26240  nbumgrvtx  26242  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  nbupgrres  26266  cplgr3v  26331  cusgrexilem2  26338  usgredgsscusgredg  26355  1hegrvtxdg1r  26404  1egrvtxdg1r  26406  1egrvtxdg0  26407  pthdadjvtx  26626  pthdlem2lem  26663  wspniunwspnon  26819  umgr2cwwk2dif  26941  3pthdlem1  27024  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  frgr3v  27139  1to3vfriswmgr  27144  frgrwopreglem5a  27175  frgrwopreglem3  27178  frgrhash2wsp  27196  staddi  29105  ornglmullt  29807  orngrmullt  29808  orngmullt  29809  ofldlt1  29813  ofldchr  29814  isarchiofld  29817  psgnfzto1stlem  29850  1smat1  29870  submateqlem1  29873  madjusmdetlem2  29894  ordtconnlem1  29970  esumrnmpt2  30130  cntnevol  30291  signstfveq0a  30653  repr0  30689  reprlt  30697  reprinfz1  30700  derangenlem  31153  subfacp1lem1  31161  subfacp1lem3  31164  subfacp1lem5  31166  noseponlem  31817  nosep1o  31832  nosupbnd2lem1  31861  noetalem3  31865  slerec  31923  dfrdg4  32058  ifscgr  32151  cgrxfr  32162  btwnconn1lem8  32201  btwnconn3  32210  segcon2  32212  broutsideof3  32233  outsideoftr  32236  outsideofeq  32237  outsideofeu  32238  lineunray  32254  lineelsb2  32255  linethru  32260  unbdqndv2lem2  32501  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem14  32516  bj-bary1lem  33160  bj-bary1lem1  33161  bj-bary1  33162  finxpreclem2  33227  finxp1o  33229  finxpreclem6  33233  fin2solem  33395  poimirlem9  33418  poimirlem15  33424  poimirlem20  33429  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  itg2addnclem2  33462  ftc1cnnc  33484  heibor1lem  33608  maxidln0  33844  lshpnelb  34271  lsatssn0  34289  lsatcv0  34318  lsat0cv  34320  lsatexch1  34333  l1cvat  34342  atlen0  34597  cvlsupr2  34630  atcvrj2b  34718  2atlt  34725  atbtwn  34732  3noncolr2  34735  4noncolr3  34739  3dimlem3  34747  3dimlem3OLDN  34748  3dimlem4  34750  3dimlem4OLDN  34751  3dim2  34754  1cvratex  34759  1cvrat  34762  ps-1  34763  ps-2  34764  hlatexch4  34767  3atlem4  34772  3atlem6  34774  4atlem0ae  34880  4atlem0be  34881  dalemccnedd  34973  dalemrotps  34977  dalem21  34980  dalem23  34982  dalem27  34985  dalem41  34999  dalem44  35002  dalem54  35012  lnatexN  35065  lnjatN  35066  llnexchb2lem  35154  llnexchb2  35155  lhpn0  35290  lhpexle3lem  35297  lhpmatb  35317  4atexlemswapqr  35349  4atexlemc  35355  4atexlemnclw  35356  4atexlemcnd  35358  4atexlemex4  35359  4atexlemex6  35360  4atex  35362  trlat  35456  trlval4  35475  cdlemc5  35482  cdlemd4  35488  cdlemd7  35491  cdlemd9  35493  cdleme0e  35504  cdleme3b  35516  cdleme3c  35517  cdleme3e  35519  cdleme3h  35522  cdleme7aa  35529  cdleme7e  35534  cdleme7ga  35535  cdleme9  35540  cdleme11c  35548  cdleme11e  35550  cdleme11fN  35551  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme15b  35562  cdleme15c  35563  cdleme17c  35575  cdleme18b  35579  cdlemesner  35583  cdleme20zN  35588  cdleme19c  35593  cdleme19d  35594  cdleme19e  35595  cdleme20m  35611  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme22f2  35635  cdleme28b  35659  cdleme36a  35748  cdleme36m  35749  cdleme41sn4aw  35763  cdleme43bN  35778  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme4gfv  35795  cdlemeg46nlpq  35805  cdlemeg46req  35817  cdlemeg46fgN  35822  cdlemf1  35849  cdlemg8b  35916  cdlemg9a  35920  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg17pq  35960  cdlemg18a  35966  cdlemg18c  35968  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33c0  35990  trlcone  36016  cdlemg42  36017  cdlemg44a  36019  cdlemg46  36023  cdlemh1  36103  cdlemh2  36104  cdlemh  36105  cdlemj3  36111  cdlemk3  36121  cdlemki  36129  cdlemksv2  36135  cdlemk12  36138  cdlemk14  36142  cdlemk15  36143  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk21N  36161  cdlemk20  36162  cdlemk22  36181  cdlemk26-3  36194  cdlemk27-3  36195  cdlemk28-3  36196  cdlemkfid3N  36213  cdlemk11ta  36217  cdlemk47  36237  cdlemk54  36246  dia2dimlem1  36353  dochsat  36672  dochshpncl  36673  lclkrlem2b  36797  lcfrlem21  36852  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdindp4  37012  mapdheq2  37018  mapdheq2biN  37019  mapdh6aN  37024  mapdh6dN  37028  mapdh6eN  37029  mapdh6hN  37032  mapdh7eN  37037  mapdh7dN  37039  mapdh7fN  37040  mapdh8ab  37066  mapdh8ad  37068  mapdh8e  37073  mapdh9a  37079  mapdh9aOLDN  37080  hdmap1l6a  37099  hdmap1l6d  37103  hdmap1l6e  37104  hdmap1l6h  37107  hdmap1eulem  37113  hdmap1eulemOLDN  37114  hdmapval0  37125  hdmapeveclem  37126  hdmapval3lemN  37129  hdmap10lem  37131  hdmap11lem1  37133  hdmaprnlem3N  37142  hdmaprnlem9N  37149  hdmaprnlem3eN  37150  jm2.26lem3  37568  rpnnen3lem  37598  rpnnen3  37599  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  bcc0  38539  chordthmALT  39169  fnchoice  39188  refsum2cnlem1  39196  xrleneltd  39539  xrltned  39573  infleinf  39588  reclt0  39614  icoiccdif  39750  ressiooinf  39784  limcresiooub  39874  limcleqr  39876  limclner  39883  climxrre  39982  icccncfext  40100  cncfiooiccre  40108  dvnxpaek  40157  stoweidlem43  40260  stirlinglem5  40295  stirlinglem7  40297  dirkercncflem1  40320  fourierdlem24  40348  fourierdlem32  40356  fourierdlem33  40357  fourierdlem34  40358  fourierdlem35  40359  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem64  40387  fourierdlem65  40388  fourierdlem74  40397  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem91  40414  fourierdlem102  40425  fourierdlem114  40437  etransclem15  40466  etransclem24  40475  sge0rpcpnf  40638  sge0isum  40644  pimrecltpos  40919  pimiooltgt  40921  setsnidel  41347  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac1  41477  fmtnoprmfac2  41479  lighneallem1  41522  lighneallem3  41524  perfectALTVlem2  41631  nnsgrpnmnd  41818  nrhmzr  41873  lvecpsslmod  42296