Theorem necomd 3012

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

This proof depends on syntax axioms:   → wi 4   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ne 2958

This theorem is used by:  difsnb  4773  0nelop  5478  xpdifid  6164  f1ounsn  7270  resf1extb  7929  difsnen  9045  fofinf1o  9287  en2eleq  9999  en2other2  10000  ackbij1lem15  10223  infpssrlem5  10297  fin23lem24  10312  fin23lem31  10333  isf32lem9  10351  canthnumlem  10639  canthp1lem2  10644  npomex  10987  ltned  11352  lt0ne0  11686  recgt0  12067  zneo  12685  xrltne  13194  supxrbnd  13360  flltnz  13851  seqf1olem1  14084  nn0opthi  14313  hashtpg  14529  hash7g  14530  hashge3el3dif  14531  cats1un  14765  sumtp  15807  geoserg  15927  geolim  15931  geolim2  15932  tanadd  16229  ruclem6  16297  ruclem7  16298  isprm2lem  16745  isprm5  16772  oddprm  16876  pcmpt  16958  cshwshashlem3  17163  resshom  17477  ressco  17478  mrissmrcd  17702  rescco  17895  estrres  18201  chnccat  18688  chnrev  18689  chnpof1  18692  smndex2dnrinv  18983  pmtrprfv  19529  symggen  19546  dprdcntz  20086  dprdres  20106  ablfac1b  20148  01eq0ringOLD  20640  nrhmzr  20647  zrdrng  20883  ornglmullt  20983  orngrmullt  20984  orngmullt  20985  ofldlt1  20989  lbspss  21214  lspsnnecom  21254  lspindp2l  21269  lspindp2  21270  islbs3  21290  lbsextlem4  21296  lidlnz  21387  isfieldidl  21397  qsidomlem2  21492  ssdifidlprm  21497  ofldchr  21737  uvcf1  21953  frlmup2  21960  psrridm  22123  coe1tmfv2  22447  coe1tmmul  22449  dmatmul  22665  mdetralt  22776  mdetunilem2  22781  mdetunilem6  22785  mdetunilem7  22786  maducoeval2  22808  madurid  22812  fvmptnn04ifa  23018  en2top  23153  cmpfi  23576  snfil  24032  tsmsfbas  24296  zcld  24982  iccpnfhmeo  25115  xrhmeo  25116  evth  25129  minveclem3b  25598  i1fres  25875  dvcnvlem  26146  ig1peu  26343  ig1pdvds  26348  aaliou3lem9  26524  taylthlem2  26548  abelthlem2  26606  abelthlem7  26612  cos02pilt1  26702  tanregt0  26715  logcj  26782  argimgt0  26788  dvloglem  26824  logf1o2  26826  logbrec  26958  ang180lem1  26985  ang180lem2  26986  ang180lem3  26987  ang180lem4  26988  ang180lem5  26989  ang180  26990  isosctrlem3  26996  ssscongptld  26998  affineequivne  27003  angpieqvdlem  27004  angpieqvdlem2  27005  angpieqvd  27007  chordthmlem  27008  chordthmlem2  27009  chordthm  27013  asinneg  27062  ppiltx  27352  perfectlem2  27405  lgsneg  27496  lgsqr  27526  lgseisenlem4  27553  lgsquadlem1  27555  lgsquadlem3  27557  lgsquad2  27561  2lgsoddprm  27591  dchrisum0flblem1  27683  noseponlem  27839  nosep1o  27856  nosep2o  27857  nosupbnd2lem1  27890  noinfbnd2lem1  27905  noetasuplem4  27911  noetainflem4  27915  lesrec  28003  0elright  28116  tgbtwnouttr  28777  tgifscgr  28788  tgcgrxfr  28798  tglngval  28831  tgfscgr  28848  tgbtwnconn1lem3  28854  tgbtwnconn3  28857  legtrid  28871  hltr  28893  hlbtwn  28894  btwnhl1  28895  btwnhl  28897  hlcgrex  28899  hlcgreulem  28900  lncom  28906  tgisline  28911  tglineeltr  28915  tglineelsb2  28916  tglinecom  28919  tglinethru  28920  ncolncol  28931  coltr  28932  coltr3  28933  tglnpt3  28938  tglnpt4  28939  symquadlem  28977  midexlem  28980  mirlni  28983  ragcol  28990  ragcgr  28998  perpneq  29005  footexALT  29009  footexlem1  29010  footexlem2  29011  foot  29013  footne  29014  colperpexlem3  29024  mideulem2  29026  opphllem  29027  midex  29029  opphllem1  29039  opphllem2  29040  opphllem3  29041  opphllem4  29042  opphllem5  29043  opphllem6  29044  outpasch  29048  hlpasch  29049  lnopp2hpgb  29056  colhp  29063  lnincplng  29077  plngrotlem1  29080  plngrotlem2  29081  plngrot  29083  lnssplnglem  29084  lnssplng  29085  lmieu  29104  hypcgrlem1  29120  hypcgrlem2  29121  lnperpex  29124  trgcopy  29126  trgcopyeulem  29127  iscgra1  29132  cgrane2  29135  cgrane3  29136  cgrane4  29137  cgracgr  29140  cgraid  29141  cgraswap  29142  cgrcgra  29143  cgracom  29144  cgratr  29145  flatcgra  29146  cgraswaplr  29147  cgracol  29150  dfcgra2  29152  sacgr  29153  oacgr  29154  acopy  29155  acopyeu  29156  ragcgra  29157  ragsupplcgra  29159  ragraghl  29160  perpeqlem  29161  perpeq  29162  leagne2  29178  leagne3  29179  cgrg3col4  29181  tgsas1  29182  tgsas2  29184  tgasa1  29186  dfprlng2  29208  dfprlng3  29209  perpprlng  29211  prlngex  29212  prlngmolem1  29213  prlngmolem2  29214  prlngmo2  29217  prlngmid2  29222  symquadprlng  29223  prlngsymquadlem  29224  prlngsymquadopp  29226  quadcgrprlng  29227  tgaltai  29228  ttgcontlem1  29245  brbtwn2  29266  axlowdimlem15  29317  axlowdimlem16  29318  axcontlem8  29332  upgrex  29453  edglnl  29504  umgrvad2edg  29574  nbupgr  29705  nbumgrvtx  29707  nbgr2vtx1edg  29711  nbuhgr2vtx1edgb  29713  nbupgrres  29725  cplgr3v  29796  cusgrexilem2  29803  usgredgsscusgredg  29820  1hegrvtxdg1r  29869  1egrvtxdg1r  29871  1egrvtxdg0  29872  pthdadjvtx  30088  pthdlem2lem  30127  wspniunwspnon  30283  umgr2cwwk2dif  30426  3pthdlem1  30526  uhgr3cyclex  30544  upgr4cycl4dv4e  30547  frgr3v  30637  1to3vfriswmgr  30642  frgrwopreglem5a  30673  frgrwopreglem3  30676  frgrhash2wsp  30694  staddi  32609  unidifsnne  32893  ifnefals  32905  coprprop  33055  sgnval2  33091  pmtrcnel  33418  pmtrcnel2  33419  psgnfzto1stlem  33429  cycpmco2lem1  33455  cycpmco2  33462  cyc2fvx  33463  cyc3co2  33469  cycpmrn  33472  tocyccntz  33473  cyc3evpm  33479  cyc3genpmlem  33480  isarchiofld  33528  drngidlhash  33750  mxidlnzr  33759  drng0mxidl  33767  drngmxidl  33768  qsdrng  33788  dflringlem3  33795  dflring3  33796  dflring4  33797  rsprprmprmidl  33821  deg1prod  33882  vietadeg1  33977  ply1annnr  34102  constrrtll  34130  constrrtlc1  34131  constrrtcclem  34133  constrrtcc  34134  constrfin  34145  constrelextdg2  34146  cos9thpiminplylem3  34183  1smat1  34203  submateqlem1  34206  ordtconnlem1  34323  esumrnmpt2  34467  cntnevol  34627  signstfveq0a  34972  repr0  35007  reprlt  35015  reprinfz1  35018  morleylemrneab  35067  nelscottrankgt  35527  cusgredgex  35622  2cycl2d  35639  acycgr1v  35649  derangenlem  35671  subfacp1lem1  35679  subfacp1lem3  35682  subfacp1lem5  35684  fmlasucdisj  35899  dfrdg4  36451  ifscgr  36544  cgrxfr  36555  btwnconn1lem8  36594  btwnconn3  36603  segcon2  36605  broutsideof3  36626  outsideoftr  36629  outsideofeq  36630  outsideofeu  36631  lineunray  36647  lineelsb2  36648  linethru  36653  mh-inf3f1  37080  mh-inf3sn  37081  unbdqndv2lem2  37127  knoppndvlem1  37129  knoppndvlem2  37130  knoppndvlem7  37135  knoppndvlem14  37142  bj-bary1lem  37982  bj-bary1lem1  37983  bj-bary1  37984  finxpreclem2  38064  finxp1o  38066  finxpreclem6  38070  fin2solem  38285  poimirlem9  38308  poimirlem15  38314  poimirlem20  38319  poimirlem24  38323  poimirlem25  38324  poimirlem27  38326  itg2addnclem2  38351  ftc1cnnc  38371  heibor1lem  38488  maxidln0  38724  lshpnelb  39786  lsatssn0  39804  lsatcv0  39833  lsat0cv  39835  lsatexch1  39848  l1cvat  39857  atlen0  40112  cvlsupr2  40145  atcvrj2b  40234  2atlt  40241  atbtwn  40248  3noncolr2  40251  4noncolr3  40255  3dimlem3  40263  3dimlem3OLDN  40264  3dimlem4  40266  3dimlem4OLDN  40267  3dim2  40270  1cvratex  40275  1cvrat  40278  ps-1  40279  ps-2  40280  hlatexch4  40283  3atlem4  40288  3atlem6  40290  4atlem0ae  40396  4atlem0be  40397  dalemccnedd  40489  dalemrotps  40493  dalem21  40496  dalem23  40498  dalem27  40501  dalem41  40515  dalem44  40518  dalem54  40528  lnatexN  40581  lnjatN  40582  llnexchb2lem  40670  llnexchb2  40671  lhpn0  40806  lhpexle3lem  40813  lhpmatb  40833  4atexlemswapqr  40865  4atexlemc  40871  4atexlemnclw  40872  4atexlemcnd  40874  4atexlemex4  40875  4atexlemex6  40876  4atex  40878  trlat  40971  trlval4  40990  cdlemc5  40997  cdlemd4  41003  cdlemd7  41006  cdlemd9  41008  cdleme0e  41019  cdleme3b  41031  cdleme3c  41032  cdleme3e  41034  cdleme3h  41037  cdleme7aa  41044  cdleme7e  41049  cdleme7ga  41050  cdleme9  41055  cdleme11c  41063  cdleme11e  41065  cdleme11fN  41066  cdleme11h  41068  cdleme11j  41069  cdleme11k  41070  cdleme15b  41077  cdleme15c  41078  cdleme17c  41090  cdleme18b  41094  cdlemesner  41098  cdleme20zN  41103  cdleme19c  41107  cdleme19d  41108  cdleme19e  41109  cdleme20m  41125  cdleme21a  41127  cdleme21b  41128  cdleme21c  41129  cdleme22f2  41149  cdleme28b  41173  cdleme36a  41262  cdleme36m  41263  cdleme41sn4aw  41277  cdleme43bN  41292  cdleme43dN  41294  cdleme46f2g2  41295  cdleme46f2g1  41296  cdleme4gfv  41309  cdlemeg46nlpq  41319  cdlemeg46req  41331  cdlemeg46fgN  41336  cdlemf1  41363  cdlemg8b  41430  cdlemg9a  41434  cdlemg12g  41451  cdlemg12  41452  cdlemg13a  41453  cdlemg17pq  41474  cdlemg18a  41480  cdlemg18c  41482  cdlemg19a  41485  cdlemg19  41486  cdlemg21  41488  cdlemg31b0N  41496  cdlemg31b0a  41497  cdlemg31c  41501  cdlemg33b0  41503  cdlemg33c0  41504  trlcone  41530  cdlemg42  41531  cdlemg44a  41533  cdlemg46  41537  cdlemh1  41617  cdlemh2  41618  cdlemh  41619  cdlemj3  41625  cdlemk3  41635  cdlemki  41643  cdlemksv2  41649  cdlemk12  41652  cdlemk14  41656  cdlemk15  41657  cdlemk7u  41672  cdlemk11u  41673  cdlemk12u  41674  cdlemk21N  41675  cdlemk20  41676  cdlemk22  41695  cdlemk26-3  41708  cdlemk27-3  41709  cdlemk28-3  41710  cdlemkfid3N  41727  cdlemk11ta  41731  cdlemk47  41751  cdlemk54  41760  dia2dimlem1  41866  dochsat  42185  dochshpncl  42186  lclkrlem2b  42310  lcfrlem21  42365  baerlem5amN  42518  baerlem5bmN  42519  baerlem5abmN  42520  mapdindp4  42525  mapdheq2  42531  mapdheq2biN  42532  mapdh6aN  42537  mapdh6dN  42541  mapdh6eN  42542  mapdh6hN  42545  mapdh7eN  42550  mapdh7dN  42552  mapdh7fN  42553  mapdh8ab  42579  mapdh8ad  42581  mapdh8e  42586  mapdh9a  42591  mapdh9aOLDN  42592  hdmap1l6a  42611  hdmap1l6d  42615  hdmap1l6e  42616  hdmap1l6h  42619  hdmap1eulem  42624  hdmap1eulemOLDN  42625  hdmapval0  42635  hdmapeveclem  42636  hdmapval3lemN  42639  hdmap10lem  42641  hdmap11lem1  42643  hdmaprnlem3N  42652  hdmaprnlem9N  42659  hdmaprnlem3eN  42660  fzne2d  42775  lcmineqlem11  42834  3lexlogpow5ineq1  42849  3lexlogpow5ineq2  42850  3lexlogpow5ineq4  42851  3lexlogpow5ineq3  42852  3lexlogpow2ineq1  42853  3lexlogpow2ineq2  42854  3lexlogpow5ineq5  42855  aks4d1lem1  42857  dvrelog2b  42861  dvrelogpow2b  42863  aks4d1p1p3  42864  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p2  42872  aks4d1p3  42873  aks4d1p5  42875  aks4d1p6  42876  aks4d1p7d1  42877  aks4d1p7  42878  aks4d1p8d3  42881  aks4d1p8  42882  aks4d1p9  42883  fldhmf1  42885  aks6d1c2p2  42914  hashscontpow  42917  aks6d1c3  42918  aks6d1c5lem2  42933  2np3bcnp1  42939  2ap1caineq  42940  sticksstones1  42941  sticksstones2  42942  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  sticksstones22  42963  aks6d1c6lem4  42968  aks6d1c7lem2  42976  unitscyglem2  42991  unitscyglem4  42993  aks5lem8  42996  xppss12  43028  mhpind  43354  jm2.26lem3  43756  rpnnen3lem  43786  rpnnen3  43787  imo72b2lem2  44921  imo72b2  44926  mnuprdlem1  45010  bcc0  45078  chordthmALT  45669  fnchoice  45777  refsum2cnlem1  45785  xrleneltd  46067  xrltned  46101  infleinf  46115  reclt0  46134  icoiccdif  46268  ressiooinf  46301  limcresiooub  46384  limcleqr  46386  limclner  46393  climxrre  46492  icccncfext  46629  cncfiooiccre  46637  dvnxpaek  46684  stoweidlem43  46785  stirlinglem5  46820  stirlinglem7  46822  dirkercncflem1  46845  fourierdlem24  46873  fourierdlem32  46881  fourierdlem33  46882  fourierdlem34  46883  fourierdlem35  46884  fourierdlem46  46894  fourierdlem48  46896  fourierdlem49  46897  fourierdlem64  46912  fourierdlem65  46913  fourierdlem74  46922  fourierdlem76  46924  fourierdlem79  46927  fourierdlem81  46929  fourierdlem91  46939  fourierdlem102  46950  fourierdlem114  46962  etransclem15  46991  etransclem24  47000  sge0rpcpnf  47163  sge0isum  47169  pimrecltpos  47450  sqrtnnaa  47632  m1modne  48119  minusmod5ne  48120  m1modnep2mod  48123  modmknepk  48133  modm2nep1  48137  modm1nep2  48139  setsnidel  48154  odz2prm2pw  48343  fmtnoprmfac1lem  48344  fmtnoprmfac1  48345  fmtnoprmfac2  48347  lighneallem1  48385  lighneallem3  48387  perfectALTVlem2  48515  usgrgrtrirex  48743  isubgr3stgrlem6  48764  gpgusgralem  48849  gpg3nbgrvtx0  48869  pgnioedg1  48901  pgnioedg2  48902  pgnioedg5  48905  nnsgrpnmnd  48971  smprngprmrng  49132  lvecpsslmod  49315  affinecomb1  49510  affinecomb2  49511  1subrec1sub  49513  rrx2plord2  49530  line  49540  rrxline  49542  eenglngeehlnmlem2  49546  rrx2vlinest  49549  line2xlem  49561  2itscp  49589