Theorem necomd 2996

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

Syntax hints:   → wi 4   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  difsnb  4806  0nelop  5501  xpdifid  6188  f1ounsn  7292  resf1extb  7956  difsnen  9093  fofinf1o  9372  en2eleq  10048  en2other2  10049  ackbij1lem15  10273  infpssrlem5  10347  fin23lem24  10362  fin23lem31  10383  isf32lem9  10401  canthnumlem  10688  canthp1lem2  10693  npomex  11036  ltned  11397  lt0ne0  11729  recgt0  12113  zneo  12701  xrltne  13205  supxrbnd  13370  flltnz  13851  seqf1olem1  14082  nn0opthi  14309  hashtpg  14524  hash7g  14525  hashge3el3dif  14526  cats1un  14759  sumtp  15785  geoserg  15902  geolim  15906  geolim2  15907  tanadd  16203  ruclem6  16271  ruclem7  16272  isprm2lem  16718  isprm5  16744  oddprm  16848  pcmpt  16930  cshwshashlem3  17135  resshom  17463  ressco  17464  mrissmrcd  17683  rescco  17876  estrres  18184  smndex2dnrinv  18928  pmtrprfv  19471  symggen  19488  dprdcntz  20028  dprdres  20048  ablfac1b  20090  01eq0ringOLD  20531  nrhmzr  20537  lbspss  21081  lspsnnecom  21121  lspindp2l  21136  lspindp2  21137  islbs3  21157  lbsextlem4  21163  sralemOLD  21176  lidlnz  21252  uvcf1  21812  frlmup2  21819  psrridm  21983  coe1tmfv2  22278  coe1tmmul  22280  dmatmul  22503  mdetralt  22614  mdetunilem2  22619  mdetunilem6  22623  mdetunilem7  22624  maducoeval2  22646  madurid  22650  fvmptnn04ifa  22856  en2top  22992  cmpfi  23416  snfil  23872  tsmsfbas  24136  zcld  24835  iccpnfhmeo  24976  xrhmeo  24977  evth  24991  minveclem3b  25462  i1fres  25740  dvcnvlem  26014  ig1peu  26214  ig1pdvds  26219  aaliou3lem9  26392  taylthlem2  26416  taylthlem2OLD  26417  abelthlem2  26476  abelthlem7  26482  cos02pilt1  26568  tanregt0  26581  logcj  26648  argimgt0  26654  dvloglem  26690  logf1o2  26692  logbrec  26825  ang180lem1  26852  ang180lem2  26853  ang180lem3  26854  ang180lem4  26855  ang180lem5  26856  ang180  26857  isosctrlem3  26863  ssscongptld  26865  affineequivne  26870  angpieqvdlem  26871  angpieqvdlem2  26872  angpieqvd  26874  chordthmlem  26875  chordthmlem2  26876  chordthm  26880  asinneg  26929  ppiltx  27220  perfectlem2  27274  lgsneg  27365  lgsqr  27395  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem3  27426  lgsquad2  27430  2lgsoddprm  27460  dchrisum0flblem1  27552  noseponlem  27709  nosep1o  27726  nosep2o  27727  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  slerec  27864  0elright  27949  tgbtwnouttr  28505  tgifscgr  28516  tgcgrxfr  28526  tglngval  28559  tgfscgr  28576  tgbtwnconn1lem3  28582  tgbtwnconn3  28585  legtrid  28599  hltr  28618  hlbtwn  28619  btwnhl1  28620  btwnhl  28622  hlcgrex  28624  hlcgreulem  28625  lncom  28630  tgisline  28635  tglineeltr  28639  tglineelsb2  28640  tglinecom  28643  tglinethru  28644  ncolncol  28654  coltr  28655  coltr3  28656  symquadlem  28697  midexlem  28700  ragcol  28707  ragcgr  28715  perpneq  28722  footexALT  28726  footexlem1  28727  footexlem2  28728  foot  28730  footne  28731  colperpexlem3  28740  mideulem2  28742  opphllem  28743  midex  28745  opphllem1  28755  opphllem2  28756  opphllem3  28757  opphllem4  28758  opphllem5  28759  opphllem6  28760  outpasch  28763  hlpasch  28764  lnopp2hpgb  28771  colhp  28778  lmieu  28792  hypcgrlem1  28807  hypcgrlem2  28808  lnperpex  28811  trgcopy  28812  trgcopyeulem  28813  iscgra1  28818  cgrane2  28821  cgrane3  28822  cgrane4  28823  cgracgr  28826  cgraid  28827  cgraswap  28828  cgrcgra  28829  cgracom  28830  cgratr  28831  flatcgra  28832  cgraswaplr  28833  cgracol  28836  dfcgra2  28838  sacgr  28839  oacgr  28840  acopy  28841  acopyeu  28842  leagne2  28858  leagne3  28859  cgrg3col4  28861  tgsas1  28862  tgsas2  28864  tgasa1  28866  ttgcontlem1  28899  cchhllemOLD  28902  brbtwn2  28920  axlowdimlem15  28971  axlowdimlem16  28972  axcontlem8  28986  upgrex  29109  edglnl  29160  umgrvad2edg  29230  nbupgr  29361  nbumgrvtx  29363  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nbupgrres  29381  cplgr3v  29452  cusgrexilem2  29459  usgredgsscusgredg  29477  1hegrvtxdg1r  29526  1egrvtxdg1r  29528  1egrvtxdg0  29529  pthdadjvtx  29748  pthdlem2lem  29787  wspniunwspnon  29943  umgr2cwwk2dif  30083  3pthdlem1  30183  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  frgr3v  30294  1to3vfriswmgr  30299  frgrwopreglem5a  30330  frgrwopreglem3  30333  frgrhash2wsp  30351  staddi  32265  unidifsnne  32554  ifnefals  32561  coprprop  32708  pmtrcnel  33109  pmtrcnel2  33110  psgnfzto1stlem  33120  cycpmco2lem1  33146  cycpmco2  33153  cyc2fvx  33154  cyc3co2  33160  cycpmrn  33163  tocyccntz  33164  cyc3evpm  33170  cyc3genpmlem  33171  ornglmullt  33337  orngrmullt  33338  orngmullt  33339  ofldlt1  33343  ofldchr  33344  isarchiofld  33347  drngidlhash  33462  qsidomlem2  33481  ssdifidlprm  33486  mxidlnzr  33495  drng0mxidl  33504  drngmxidl  33505  qsdrng  33525  rsprprmprmidl  33550  ply1annnr  33746  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  constrfin  33787  constrelextdg2  33788  1smat1  33803  submateqlem1  33806  ordtconnlem1  33923  esumrnmpt2  34069  cntnevol  34229  signstfveq0a  34591  repr0  34626  reprlt  34634  reprinfz1  34637  cusgredgex  35127  2cycl2d  35144  acycgr1v  35154  derangenlem  35176  subfacp1lem1  35184  subfacp1lem3  35187  subfacp1lem5  35189  fmlasucdisj  35404  dfrdg4  35952  ifscgr  36045  cgrxfr  36056  btwnconn1lem8  36095  btwnconn3  36104  segcon2  36106  broutsideof3  36127  outsideoftr  36130  outsideofeq  36131  outsideofeu  36132  lineunray  36148  lineelsb2  36149  linethru  36154  unbdqndv2lem2  36511  knoppndvlem1  36513  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem14  36526  bj-bary1lem  37311  bj-bary1lem1  37312  bj-bary1  37313  finxpreclem2  37391  finxp1o  37393  finxpreclem6  37397  fin2solem  37613  poimirlem9  37636  poimirlem15  37642  poimirlem20  37647  poimirlem24  37651  poimirlem25  37652  poimirlem27  37654  itg2addnclem2  37679  ftc1cnnc  37699  heibor1lem  37816  maxidln0  38052  lshpnelb  38985  lsatssn0  39003  lsatcv0  39032  lsat0cv  39034  lsatexch1  39047  l1cvat  39056  atlen0  39311  cvlsupr2  39344  atcvrj2b  39434  2atlt  39441  atbtwn  39448  3noncolr2  39451  4noncolr3  39455  3dimlem3  39463  3dimlem3OLDN  39464  3dimlem4  39466  3dimlem4OLDN  39467  3dim2  39470  1cvratex  39475  1cvrat  39478  ps-1  39479  ps-2  39480  hlatexch4  39483  3atlem4  39488  3atlem6  39490  4atlem0ae  39596  4atlem0be  39597  dalemccnedd  39689  dalemrotps  39693  dalem21  39696  dalem23  39698  dalem27  39701  dalem41  39715  dalem44  39718  dalem54  39728  lnatexN  39781  lnjatN  39782  llnexchb2lem  39870  llnexchb2  39871  lhpn0  40006  lhpexle3lem  40013  lhpmatb  40033  4atexlemswapqr  40065  4atexlemc  40071  4atexlemnclw  40072  4atexlemcnd  40074  4atexlemex4  40075  4atexlemex6  40076  4atex  40078  trlat  40171  trlval4  40190  cdlemc5  40197  cdlemd4  40203  cdlemd7  40206  cdlemd9  40208  cdleme0e  40219  cdleme3b  40231  cdleme3c  40232  cdleme3e  40234  cdleme3h  40237  cdleme7aa  40244  cdleme7e  40249  cdleme7ga  40250  cdleme9  40255  cdleme11c  40263  cdleme11e  40265  cdleme11fN  40266  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme15b  40277  cdleme15c  40278  cdleme17c  40290  cdleme18b  40294  cdlemesner  40298  cdleme20zN  40303  cdleme19c  40307  cdleme19d  40308  cdleme19e  40309  cdleme20m  40325  cdleme21a  40327  cdleme21b  40328  cdleme21c  40329  cdleme22f2  40349  cdleme28b  40373  cdleme36a  40462  cdleme36m  40463  cdleme41sn4aw  40477  cdleme43bN  40492  cdleme43dN  40494  cdleme46f2g2  40495  cdleme46f2g1  40496  cdleme4gfv  40509  cdlemeg46nlpq  40519  cdlemeg46req  40531  cdlemeg46fgN  40536  cdlemf1  40563  cdlemg8b  40630  cdlemg9a  40634  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg17pq  40674  cdlemg18a  40680  cdlemg18c  40682  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg31b0N  40696  cdlemg31b0a  40697  cdlemg31c  40701  cdlemg33b0  40703  cdlemg33c0  40704  trlcone  40730  cdlemg42  40731  cdlemg44a  40733  cdlemg46  40737  cdlemh1  40817  cdlemh2  40818  cdlemh  40819  cdlemj3  40825  cdlemk3  40835  cdlemki  40843  cdlemksv2  40849  cdlemk12  40852  cdlemk14  40856  cdlemk15  40857  cdlemk7u  40872  cdlemk11u  40873  cdlemk12u  40874  cdlemk21N  40875  cdlemk20  40876  cdlemk22  40895  cdlemk26-3  40908  cdlemk27-3  40909  cdlemk28-3  40910  cdlemkfid3N  40927  cdlemk11ta  40931  cdlemk47  40951  cdlemk54  40960  dia2dimlem1  41066  dochsat  41385  dochshpncl  41386  lclkrlem2b  41510  lcfrlem21  41565  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdindp4  41725  mapdheq2  41731  mapdheq2biN  41732  mapdh6aN  41737  mapdh6dN  41741  mapdh6eN  41742  mapdh6hN  41745  mapdh7eN  41750  mapdh7dN  41752  mapdh7fN  41753  mapdh8ab  41779  mapdh8ad  41781  mapdh8e  41786  mapdh9a  41791  mapdh9aOLDN  41792  hdmap1l6a  41811  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6h  41819  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmapval0  41835  hdmapeveclem  41836  hdmapval3lemN  41839  hdmap10lem  41841  hdmap11lem1  41843  hdmaprnlem3N  41852  hdmaprnlem9N  41859  hdmaprnlem3eN  41860  fzne2d  41981  lcmineqlem11  42040  3lexlogpow5ineq1  42055  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8d3  42087  aks4d1p8  42088  aks4d1p9  42089  fldhmf1  42091  aks6d1c2p2  42120  hashscontpow  42123  aks6d1c3  42124  aks6d1c5lem2  42139  2np3bcnp1  42145  2ap1caineq  42146  sticksstones1  42147  sticksstones2  42148  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem4  42174  aks6d1c7lem2  42182  unitscyglem2  42197  unitscyglem4  42199  aks5lem8  42202  metakunt7  42212  metakunt12  42217  metakunt22  42227  xppss12  42268  mhpind  42604  jm2.26lem3  43013  rpnnen3lem  43043  rpnnen3  43044  imo72b2lem2  44180  imo72b2  44185  mnuprdlem1  44291  bcc0  44359  chordthmALT  44953  fnchoice  45034  refsum2cnlem1  45042  xrleneltd  45334  xrltned  45368  infleinf  45383  reclt0  45402  icoiccdif  45537  ressiooinf  45570  limcresiooub  45657  limcleqr  45659  limclner  45666  climxrre  45765  icccncfext  45902  cncfiooiccre  45910  dvnxpaek  45957  stoweidlem43  46058  stirlinglem5  46093  stirlinglem7  46095  dirkercncflem1  46118  fourierdlem24  46146  fourierdlem32  46154  fourierdlem33  46155  fourierdlem34  46156  fourierdlem35  46157  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem91  46212  fourierdlem102  46223  fourierdlem114  46235  etransclem15  46264  etransclem24  46273  sge0rpcpnf  46436  sge0isum  46442  pimrecltpos  46723  pimiooltgt  46725  m1modne  47350  minusmod5ne  47351  m1modnep2mod  47354  setsnidel  47364  odz2prm2pw  47550  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  fmtnoprmfac2  47554  lighneallem1  47592  lighneallem3  47594  perfectALTVlem2  47709  usgrgrtrirex  47917  isubgr3stgrlem6  47938  gpgusgralem  48011  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  nnsgrpnmnd  48094  lvecpsslmod  48424  affinecomb1  48623  affinecomb2  48624  1subrec1sub  48626  rrx2plord2  48643  line  48653  rrxline  48655  eenglngeehlnmlem2  48659  rrx2vlinest  48662  line2xlem  48674  2itscp  48702