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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

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

This theorem is referenced by:  difsnb  4741  0nelop  5439  xpdifid  6121  f1ounsn  7216  resf1extb  7874  difsnen  8986  fofinf1o  9231  en2eleq  9919  en2other2  9920  ackbij1lem15  10144  infpssrlem5  10218  fin23lem24  10233  fin23lem31  10254  isf32lem9  10272  canthnumlem  10560  canthp1lem2  10565  npomex  10908  ltned  11271  lt0ne0  11605  recgt0  11990  zneo  12601  xrltne  13103  supxrbnd  13269  flltnz  13759  seqf1olem1  13992  nn0opthi  14221  hashtpg  14436  hash7g  14437  hashge3el3dif  14438  cats1un  14672  sumtp  15700  geoserg  15820  geolim  15824  geolim2  15825  tanadd  16123  ruclem6  16191  ruclem7  16192  isprm2lem  16639  isprm5  16666  oddprm  16770  pcmpt  16852  cshwshashlem3  17057  resshom  17370  ressco  17371  mrissmrcd  17595  rescco  17788  estrres  18094  chnccat  18581  chnrev  18582  chnpof1  18585  smndex2dnrinv  18875  pmtrprfv  19417  symggen  19434  dprdcntz  19974  dprdres  19994  ablfac1b  20036  01eq0ringOLD  20497  nrhmzr  20503  ornglmullt  20835  orngrmullt  20836  orngmullt  20837  ofldlt1  20841  lbspss  21066  lspsnnecom  21106  lspindp2l  21121  lspindp2  21122  islbs3  21142  lbsextlem4  21148  lidlnz  21229  ofldchr  21545  uvcf1  21761  frlmup2  21768  psrridm  21930  coe1tmfv2  22228  coe1tmmul  22230  dmatmul  22450  mdetralt  22561  mdetunilem2  22566  mdetunilem6  22570  mdetunilem7  22571  maducoeval2  22593  madurid  22597  fvmptnn04ifa  22803  en2top  22938  cmpfi  23361  snfil  23817  tsmsfbas  24081  zcld  24767  iccpnfhmeo  24900  xrhmeo  24901  evth  24914  minveclem3b  25383  i1fres  25660  dvcnvlem  25931  ig1peu  26128  ig1pdvds  26133  aaliou3lem9  26304  taylthlem2  26327  abelthlem2  26385  abelthlem7  26391  cos02pilt1  26478  tanregt0  26491  logcj  26558  argimgt0  26564  dvloglem  26600  logf1o2  26602  logbrec  26734  ang180lem1  26761  ang180lem2  26762  ang180lem3  26763  ang180lem4  26764  ang180lem5  26765  ang180  26766  isosctrlem3  26772  ssscongptld  26774  affineequivne  26779  angpieqvdlem  26780  angpieqvdlem2  26781  angpieqvd  26783  chordthmlem  26784  chordthmlem2  26785  chordthm  26789  asinneg  26838  ppiltx  27128  perfectlem2  27181  lgsneg  27272  lgsqr  27302  lgseisenlem4  27329  lgsquadlem1  27331  lgsquadlem3  27333  lgsquad2  27337  2lgsoddprm  27367  dchrisum0flblem1  27459  noseponlem  27616  nosep1o  27633  nosep2o  27634  nosupbnd2lem1  27667  noinfbnd2lem1  27682  noetasuplem4  27688  noetainflem4  27692  lesrec  27779  0elright  27892  tgbtwnouttr  28553  tgifscgr  28564  tgcgrxfr  28574  tglngval  28607  tgfscgr  28624  tgbtwnconn1lem3  28630  tgbtwnconn3  28633  legtrid  28647  hltr  28666  hlbtwn  28667  btwnhl1  28668  btwnhl  28670  hlcgrex  28672  hlcgreulem  28673  lncom  28678  tgisline  28683  tglineeltr  28687  tglineelsb2  28688  tglinecom  28691  tglinethru  28692  ncolncol  28702  coltr  28703  coltr3  28704  symquadlem  28745  midexlem  28748  ragcol  28755  ragcgr  28763  perpneq  28770  footexALT  28774  footexlem1  28775  footexlem2  28776  foot  28778  footne  28779  colperpexlem3  28788  mideulem2  28790  opphllem  28791  midex  28793  opphllem1  28803  opphllem2  28804  opphllem3  28805  opphllem4  28806  opphllem5  28807  opphllem6  28808  outpasch  28811  hlpasch  28812  lnopp2hpgb  28819  colhp  28826  lmieu  28840  hypcgrlem1  28855  hypcgrlem2  28856  lnperpex  28859  trgcopy  28860  trgcopyeulem  28861  iscgra1  28866  cgrane2  28869  cgrane3  28870  cgrane4  28871  cgracgr  28874  cgraid  28875  cgraswap  28876  cgrcgra  28877  cgracom  28878  cgratr  28879  flatcgra  28880  cgraswaplr  28881  cgracol  28884  dfcgra2  28886  sacgr  28887  oacgr  28888  acopy  28889  acopyeu  28890  leagne2  28906  leagne3  28907  cgrg3col4  28909  tgsas1  28910  tgsas2  28912  tgasa1  28914  ttgcontlem1  28941  brbtwn2  28962  axlowdimlem15  29013  axlowdimlem16  29014  axcontlem8  29028  upgrex  29149  edglnl  29200  umgrvad2edg  29270  nbupgr  29401  nbumgrvtx  29403  nbgr2vtx1edg  29407  nbuhgr2vtx1edgb  29409  nbupgrres  29421  cplgr3v  29492  cusgrexilem2  29499  usgredgsscusgredg  29516  1hegrvtxdg1r  29565  1egrvtxdg1r  29567  1egrvtxdg0  29568  pthdadjvtx  29784  pthdlem2lem  29823  wspniunwspnon  29979  umgr2cwwk2dif  30122  3pthdlem1  30222  uhgr3cyclex  30240  upgr4cycl4dv4e  30243  frgr3v  30333  1to3vfriswmgr  30338  frgrwopreglem5a  30369  frgrwopreglem3  30372  frgrhash2wsp  30390  staddi  32305  unidifsnne  32594  ifnefals  32606  coprprop  32760  sgnval2  32796  pmtrcnel  33138  pmtrcnel2  33139  psgnfzto1stlem  33149  cycpmco2lem1  33175  cycpmco2  33182  cyc2fvx  33183  cyc3co2  33189  cycpmrn  33192  tocyccntz  33193  cyc3evpm  33199  cyc3genpmlem  33200  isarchiofld  33248  drngidlhash  33482  qsidomlem2  33501  ssdifidlprm  33506  mxidlnzr  33515  drng0mxidl  33524  drngmxidl  33525  qsdrng  33545  rsprprmprmidl  33570  deg1prod  33631  vietadeg1  33710  ply1annnr  33835  constrrtll  33863  constrrtlc1  33864  constrrtcclem  33866  constrrtcc  33867  constrfin  33878  constrelextdg2  33879  cos9thpiminplylem3  33916  1smat1  33936  submateqlem1  33939  ordtconnlem1  34056  esumrnmpt2  34200  cntnevol  34360  signstfveq0a  34708  repr0  34743  reprlt  34751  reprinfz1  34754  cusgredgex  35292  2cycl2d  35309  acycgr1v  35319  derangenlem  35341  subfacp1lem1  35349  subfacp1lem3  35352  subfacp1lem5  35354  fmlasucdisj  35569  dfrdg4  36121  ifscgr  36214  cgrxfr  36225  btwnconn1lem8  36264  btwnconn3  36273  segcon2  36275  broutsideof3  36296  outsideoftr  36299  outsideofeq  36300  outsideofeu  36301  lineunray  36317  lineelsb2  36318  linethru  36323  mh-inf3f1  36711  mh-inf3sn  36712  unbdqndv2lem2  36758  knoppndvlem1  36760  knoppndvlem2  36761  knoppndvlem7  36766  knoppndvlem14  36773  bj-bary1lem  37612  bj-bary1lem1  37613  bj-bary1  37614  finxpreclem2  37694  finxp1o  37696  finxpreclem6  37700  fin2solem  37915  poimirlem9  37938  poimirlem15  37944  poimirlem20  37949  poimirlem24  37953  poimirlem25  37954  poimirlem27  37956  itg2addnclem2  37981  ftc1cnnc  38001  heibor1lem  38118  maxidln0  38354  lshpnelb  39418  lsatssn0  39436  lsatcv0  39465  lsat0cv  39467  lsatexch1  39480  l1cvat  39489  atlen0  39744  cvlsupr2  39777  atcvrj2b  39866  2atlt  39873  atbtwn  39880  3noncolr2  39883  4noncolr3  39887  3dimlem3  39895  3dimlem3OLDN  39896  3dimlem4  39898  3dimlem4OLDN  39899  3dim2  39902  1cvratex  39907  1cvrat  39910  ps-1  39911  ps-2  39912  hlatexch4  39915  3atlem4  39920  3atlem6  39922  4atlem0ae  40028  4atlem0be  40029  dalemccnedd  40121  dalemrotps  40125  dalem21  40128  dalem23  40130  dalem27  40133  dalem41  40147  dalem44  40150  dalem54  40160  lnatexN  40213  lnjatN  40214  llnexchb2lem  40302  llnexchb2  40303  lhpn0  40438  lhpexle3lem  40445  lhpmatb  40465  4atexlemswapqr  40497  4atexlemc  40503  4atexlemnclw  40504  4atexlemcnd  40506  4atexlemex4  40507  4atexlemex6  40508  4atex  40510  trlat  40603  trlval4  40622  cdlemc5  40629  cdlemd4  40635  cdlemd7  40638  cdlemd9  40640  cdleme0e  40651  cdleme3b  40663  cdleme3c  40664  cdleme3e  40666  cdleme3h  40669  cdleme7aa  40676  cdleme7e  40681  cdleme7ga  40682  cdleme9  40687  cdleme11c  40695  cdleme11e  40697  cdleme11fN  40698  cdleme11h  40700  cdleme11j  40701  cdleme11k  40702  cdleme15b  40709  cdleme15c  40710  cdleme17c  40722  cdleme18b  40726  cdlemesner  40730  cdleme20zN  40735  cdleme19c  40739  cdleme19d  40740  cdleme19e  40741  cdleme20m  40757  cdleme21a  40759  cdleme21b  40760  cdleme21c  40761  cdleme22f2  40781  cdleme28b  40805  cdleme36a  40894  cdleme36m  40895  cdleme41sn4aw  40909  cdleme43bN  40924  cdleme43dN  40926  cdleme46f2g2  40927  cdleme46f2g1  40928  cdleme4gfv  40941  cdlemeg46nlpq  40951  cdlemeg46req  40963  cdlemeg46fgN  40968  cdlemf1  40995  cdlemg8b  41062  cdlemg9a  41066  cdlemg12g  41083  cdlemg12  41084  cdlemg13a  41085  cdlemg17pq  41106  cdlemg18a  41112  cdlemg18c  41114  cdlemg19a  41117  cdlemg19  41118  cdlemg21  41120  cdlemg31b0N  41128  cdlemg31b0a  41129  cdlemg31c  41133  cdlemg33b0  41135  cdlemg33c0  41136  trlcone  41162  cdlemg42  41163  cdlemg44a  41165  cdlemg46  41169  cdlemh1  41249  cdlemh2  41250  cdlemh  41251  cdlemj3  41257  cdlemk3  41267  cdlemki  41275  cdlemksv2  41281  cdlemk12  41284  cdlemk14  41288  cdlemk15  41289  cdlemk7u  41304  cdlemk11u  41305  cdlemk12u  41306  cdlemk21N  41307  cdlemk20  41308  cdlemk22  41327  cdlemk26-3  41340  cdlemk27-3  41341  cdlemk28-3  41342  cdlemkfid3N  41359  cdlemk11ta  41363  cdlemk47  41383  cdlemk54  41392  dia2dimlem1  41498  dochsat  41817  dochshpncl  41818  lclkrlem2b  41942  lcfrlem21  41997  baerlem5amN  42150  baerlem5bmN  42151  baerlem5abmN  42152  mapdindp4  42157  mapdheq2  42163  mapdheq2biN  42164  mapdh6aN  42169  mapdh6dN  42173  mapdh6eN  42174  mapdh6hN  42177  mapdh7eN  42182  mapdh7dN  42184  mapdh7fN  42185  mapdh8ab  42211  mapdh8ad  42213  mapdh8e  42218  mapdh9a  42223  mapdh9aOLDN  42224  hdmap1l6a  42243  hdmap1l6d  42247  hdmap1l6e  42248  hdmap1l6h  42251  hdmap1eulem  42256  hdmap1eulemOLDN  42257  hdmapval0  42267  hdmapeveclem  42268  hdmapval3lemN  42271  hdmap10lem  42273  hdmap11lem1  42275  hdmaprnlem3N  42284  hdmaprnlem9N  42291  hdmaprnlem3eN  42292  fzne2d  42407  lcmineqlem11  42466  3lexlogpow5ineq1  42481  3lexlogpow5ineq2  42482  3lexlogpow5ineq4  42483  3lexlogpow5ineq3  42484  3lexlogpow2ineq1  42485  3lexlogpow2ineq2  42486  3lexlogpow5ineq5  42487  aks4d1lem1  42489  dvrelog2b  42493  dvrelogpow2b  42495  aks4d1p1p3  42496  aks4d1p1p2  42497  aks4d1p1p4  42498  aks4d1p1p6  42500  aks4d1p1p7  42501  aks4d1p1p5  42502  aks4d1p1  42503  aks4d1p2  42504  aks4d1p3  42505  aks4d1p5  42507  aks4d1p6  42508  aks4d1p7d1  42509  aks4d1p7  42510  aks4d1p8d3  42513  aks4d1p8  42514  aks4d1p9  42515  fldhmf1  42517  aks6d1c2p2  42546  hashscontpow  42549  aks6d1c3  42550  aks6d1c5lem2  42565  2np3bcnp1  42571  2ap1caineq  42572  sticksstones1  42573  sticksstones2  42574  sticksstones10  42582  sticksstones12a  42584  sticksstones12  42585  sticksstones22  42595  aks6d1c6lem4  42600  aks6d1c7lem2  42608  unitscyglem2  42623  unitscyglem4  42625  aks5lem8  42628  xppss12  42658  mhpind  43015  jm2.26lem3  43417  rpnnen3lem  43447  rpnnen3  43448  imo72b2lem2  44582  imo72b2  44587  mnuprdlem1  44687  bcc0  44755  chordthmALT  45347  fnchoice  45448  refsum2cnlem1  45456  xrleneltd  45741  xrltned  45775  infleinf  45789  reclt0  45808  icoiccdif  45942  ressiooinf  45975  limcresiooub  46058  limcleqr  46060  limclner  46067  climxrre  46166  icccncfext  46303  cncfiooiccre  46311  dvnxpaek  46358  stoweidlem43  46459  stirlinglem5  46494  stirlinglem7  46496  dirkercncflem1  46519  fourierdlem24  46547  fourierdlem32  46555  fourierdlem33  46556  fourierdlem34  46557  fourierdlem35  46558  fourierdlem46  46568  fourierdlem48  46570  fourierdlem49  46571  fourierdlem64  46586  fourierdlem65  46587  fourierdlem74  46596  fourierdlem76  46598  fourierdlem79  46601  fourierdlem81  46603  fourierdlem91  46613  fourierdlem102  46624  fourierdlem114  46636  etransclem15  46665  etransclem24  46674  sge0rpcpnf  46837  sge0isum  46843  pimrecltpos  47124  m1modne  47790  minusmod5ne  47791  m1modnep2mod  47794  modmknepk  47804  modm2nep1  47808  modm1nep2  47810  setsnidel  47825  odz2prm2pw  48014  fmtnoprmfac1lem  48015  fmtnoprmfac1  48016  fmtnoprmfac2  48018  lighneallem1  48056  lighneallem3  48058  perfectALTVlem2  48186  usgrgrtrirex  48414  isubgr3stgrlem6  48435  gpgusgralem  48520  gpg3nbgrvtx0  48540  pgnioedg1  48572  pgnioedg2  48573  pgnioedg5  48576  nnsgrpnmnd  48642  lvecpsslmod  48971  affinecomb1  49166  affinecomb2  49167  1subrec1sub  49169  rrx2plord2  49186  line  49196  rrxline  49198  eenglngeehlnmlem2  49202  rrx2vlinest  49205  line2xlem  49217  2itscp  49245