Theorem necomd 2993

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

Syntax hints:   → wi 4   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-ne 2938

This theorem is referenced by:  difsnb  4810  0nelop  5498  xpdifid  6172  difsnen  9077  fofinf1o  9351  en2eleq  10031  en2other2  10032  ackbij1lem15  10257  infpssrlem5  10330  fin23lem24  10345  fin23lem31  10366  isf32lem9  10384  canthnumlem  10671  canthp1lem2  10676  npomex  11019  ltned  11380  lt0ne0  11710  recgt0  12090  zneo  12675  xrltne  13174  supxrbnd  13339  flltnz  13808  seqf1olem1  14038  nn0opthi  14261  hashtpg  14478  hashge3el3dif  14479  cats1un  14703  sumtp  15727  geoserg  15844  geolim  15848  geolim2  15849  tanadd  16143  ruclem6  16211  ruclem7  16212  isprm2lem  16651  isprm5  16677  oddprm  16778  pcmpt  16860  cshwshashlem3  17066  resshom  17399  ressco  17400  mrissmrcd  17619  rescco  17815  estrres  18129  smndex2dnrinv  18866  pmtrprfv  19407  symggen  19424  dprdcntz  19964  dprdres  19984  ablfac1b  20026  01eq0ringOLD  20467  nrhmzr  20473  lbspss  20966  lspsnnecom  21006  lspindp2l  21021  lspindp2  21022  islbs3  21042  lbsextlem4  21048  sralemOLD  21061  lidlnz  21136  uvcf1  21725  frlmup2  21732  psrridm  21905  coe1tmfv2  22193  coe1tmmul  22195  dmatmul  22398  mdetralt  22509  mdetunilem2  22514  mdetunilem6  22518  mdetunilem7  22519  maducoeval2  22541  madurid  22545  fvmptnn04ifa  22751  en2top  22887  cmpfi  23311  snfil  23767  tsmsfbas  24031  zcld  24728  iccpnfhmeo  24869  xrhmeo  24870  evth  24884  minveclem3b  25355  i1fres  25634  dvcnvlem  25907  ig1peu  26108  ig1pdvds  26113  aaliou3lem9  26284  taylthlem2  26308  taylthlem2OLD  26309  abelthlem2  26368  abelthlem7  26374  cos02pilt1  26459  tanregt0  26472  logcj  26539  argimgt0  26545  dvloglem  26581  logf1o2  26583  logbrec  26713  ang180lem1  26740  ang180lem2  26741  ang180lem3  26742  ang180lem4  26743  ang180lem5  26744  ang180  26745  isosctrlem3  26751  ssscongptld  26753  affineequivne  26758  angpieqvdlem  26759  angpieqvdlem2  26760  angpieqvd  26762  chordthmlem  26763  chordthmlem2  26764  chordthm  26768  asinneg  26817  ppiltx  27108  perfectlem2  27162  lgsneg  27253  lgsqr  27283  lgseisenlem4  27310  lgsquadlem1  27312  lgsquadlem3  27314  lgsquad2  27318  2lgsoddprm  27348  dchrisum0flblem1  27440  noseponlem  27596  nosep1o  27613  nosep2o  27614  nosupbnd2lem1  27647  noinfbnd2lem1  27662  noetasuplem4  27668  noetainflem4  27672  slerec  27751  0elright  27836  tgbtwnouttr  28300  tgifscgr  28311  tgcgrxfr  28321  tglngval  28354  tgfscgr  28371  tgbtwnconn1lem3  28377  tgbtwnconn3  28380  legtrid  28394  hltr  28413  hlbtwn  28414  btwnhl1  28415  btwnhl  28417  hlcgrex  28419  hlcgreulem  28420  lncom  28425  tgisline  28430  tglineeltr  28434  tglineelsb2  28435  tglinecom  28438  tglinethru  28439  ncolncol  28449  coltr  28450  coltr3  28451  symquadlem  28492  midexlem  28495  ragcol  28502  ragcgr  28510  perpneq  28517  footexALT  28521  footexlem1  28522  footexlem2  28523  foot  28525  footne  28526  colperpexlem3  28535  mideulem2  28537  opphllem  28538  midex  28540  opphllem1  28550  opphllem2  28551  opphllem3  28552  opphllem4  28553  opphllem5  28554  opphllem6  28555  outpasch  28558  hlpasch  28559  lnopp2hpgb  28566  colhp  28573  lmieu  28587  hypcgrlem1  28602  hypcgrlem2  28603  lnperpex  28606  trgcopy  28607  trgcopyeulem  28608  iscgra1  28613  cgrane2  28616  cgrane3  28617  cgrane4  28618  cgracgr  28621  cgraid  28622  cgraswap  28623  cgrcgra  28624  cgracom  28625  cgratr  28626  flatcgra  28627  cgraswaplr  28628  cgracol  28631  dfcgra2  28633  sacgr  28634  oacgr  28635  acopy  28636  acopyeu  28637  leagne2  28653  leagne3  28654  cgrg3col4  28656  tgsas1  28657  tgsas2  28659  tgasa1  28661  ttgcontlem1  28694  cchhllemOLD  28697  brbtwn2  28715  axlowdimlem15  28766  axlowdimlem16  28767  axcontlem8  28781  upgrex  28904  edglnl  28955  umgrvad2edg  29025  nbupgr  29156  nbumgrvtx  29158  nbgr2vtx1edg  29162  nbuhgr2vtx1edgb  29164  nbupgrres  29176  cplgr3v  29247  cusgrexilem2  29254  usgredgsscusgredg  29272  1hegrvtxdg1r  29321  1egrvtxdg1r  29323  1egrvtxdg0  29324  pthdadjvtx  29543  pthdlem2lem  29580  wspniunwspnon  29733  umgr2cwwk2dif  29873  3pthdlem1  29973  uhgr3cyclex  29991  upgr4cycl4dv4e  29994  frgr3v  30084  1to3vfriswmgr  30089  frgrwopreglem5a  30120  frgrwopreglem3  30123  frgrhash2wsp  30141  staddi  32055  unidifsnne  32331  ifnefals  32338  coprprop  32479  pmtrcnel  32812  pmtrcnel2  32813  psgnfzto1stlem  32821  cycpmco2lem1  32847  cycpmco2  32854  cyc2fvx  32855  cyc3co2  32861  cycpmrn  32864  tocyccntz  32865  cyc3evpm  32871  cyc3genpmlem  32872  ornglmullt  33022  orngrmullt  33023  orngmullt  33024  ofldlt1  33028  ofldchr  33029  isarchiofld  33032  drngidlhash  33150  qsidomlem2  33169  mxidlnzr  33180  drng0mxidl  33189  drngmxidl  33190  qsdrng  33208  ply1annnr  33374  1smat1  33405  submateqlem1  33408  madjusmdetlem2  33429  ordtconnlem1  33525  esumrnmpt2  33687  cntnevol  33847  signstfveq0a  34208  repr0  34243  reprlt  34251  reprinfz1  34254  cusgredgex  34731  2cycl2d  34749  acycgr1v  34759  derangenlem  34781  subfacp1lem1  34789  subfacp1lem3  34792  subfacp1lem5  34794  fmlasucdisj  35009  dfrdg4  35547  ifscgr  35640  cgrxfr  35651  btwnconn1lem8  35690  btwnconn3  35699  segcon2  35701  broutsideof3  35722  outsideoftr  35725  outsideofeq  35726  outsideofeu  35727  lineunray  35743  lineelsb2  35744  linethru  35749  unbdqndv2lem2  35985  knoppndvlem1  35987  knoppndvlem2  35988  knoppndvlem7  35993  knoppndvlem14  36000  bj-bary1lem  36789  bj-bary1lem1  36790  bj-bary1  36791  finxpreclem2  36869  finxp1o  36871  finxpreclem6  36875  fin2solem  37079  poimirlem9  37102  poimirlem15  37108  poimirlem20  37113  poimirlem24  37117  poimirlem25  37118  poimirlem27  37120  itg2addnclem2  37145  ftc1cnnc  37165  heibor1lem  37282  maxidln0  37518  lshpnelb  38456  lsatssn0  38474  lsatcv0  38503  lsat0cv  38505  lsatexch1  38518  l1cvat  38527  atlen0  38782  cvlsupr2  38815  atcvrj2b  38905  2atlt  38912  atbtwn  38919  3noncolr2  38922  4noncolr3  38926  3dimlem3  38934  3dimlem3OLDN  38935  3dimlem4  38937  3dimlem4OLDN  38938  3dim2  38941  1cvratex  38946  1cvrat  38949  ps-1  38950  ps-2  38951  hlatexch4  38954  3atlem4  38959  3atlem6  38961  4atlem0ae  39067  4atlem0be  39068  dalemccnedd  39160  dalemrotps  39164  dalem21  39167  dalem23  39169  dalem27  39172  dalem41  39186  dalem44  39189  dalem54  39199  lnatexN  39252  lnjatN  39253  llnexchb2lem  39341  llnexchb2  39342  lhpn0  39477  lhpexle3lem  39484  lhpmatb  39504  4atexlemswapqr  39536  4atexlemc  39542  4atexlemnclw  39543  4atexlemcnd  39545  4atexlemex4  39546  4atexlemex6  39547  4atex  39549  trlat  39642  trlval4  39661  cdlemc5  39668  cdlemd4  39674  cdlemd7  39677  cdlemd9  39679  cdleme0e  39690  cdleme3b  39702  cdleme3c  39703  cdleme3e  39705  cdleme3h  39708  cdleme7aa  39715  cdleme7e  39720  cdleme7ga  39721  cdleme9  39726  cdleme11c  39734  cdleme11e  39736  cdleme11fN  39737  cdleme11h  39739  cdleme11j  39740  cdleme11k  39741  cdleme15b  39748  cdleme15c  39749  cdleme17c  39761  cdleme18b  39765  cdlemesner  39769  cdleme20zN  39774  cdleme19c  39778  cdleme19d  39779  cdleme19e  39780  cdleme20m  39796  cdleme21a  39798  cdleme21b  39799  cdleme21c  39800  cdleme22f2  39820  cdleme28b  39844  cdleme36a  39933  cdleme36m  39934  cdleme41sn4aw  39948  cdleme43bN  39963  cdleme43dN  39965  cdleme46f2g2  39966  cdleme46f2g1  39967  cdleme4gfv  39980  cdlemeg46nlpq  39990  cdlemeg46req  40002  cdlemeg46fgN  40007  cdlemf1  40034  cdlemg8b  40101  cdlemg9a  40105  cdlemg12g  40122  cdlemg12  40123  cdlemg13a  40124  cdlemg17pq  40145  cdlemg18a  40151  cdlemg18c  40153  cdlemg19a  40156  cdlemg19  40157  cdlemg21  40159  cdlemg31b0N  40167  cdlemg31b0a  40168  cdlemg31c  40172  cdlemg33b0  40174  cdlemg33c0  40175  trlcone  40201  cdlemg42  40202  cdlemg44a  40204  cdlemg46  40208  cdlemh1  40288  cdlemh2  40289  cdlemh  40290  cdlemj3  40296  cdlemk3  40306  cdlemki  40314  cdlemksv2  40320  cdlemk12  40323  cdlemk14  40327  cdlemk15  40328  cdlemk7u  40343  cdlemk11u  40344  cdlemk12u  40345  cdlemk21N  40346  cdlemk20  40347  cdlemk22  40366  cdlemk26-3  40379  cdlemk27-3  40380  cdlemk28-3  40381  cdlemkfid3N  40398  cdlemk11ta  40402  cdlemk47  40422  cdlemk54  40431  dia2dimlem1  40537  dochsat  40856  dochshpncl  40857  lclkrlem2b  40981  lcfrlem21  41036  baerlem5amN  41189  baerlem5bmN  41190  baerlem5abmN  41191  mapdindp4  41196  mapdheq2  41202  mapdheq2biN  41203  mapdh6aN  41208  mapdh6dN  41212  mapdh6eN  41213  mapdh6hN  41216  mapdh7eN  41221  mapdh7dN  41223  mapdh7fN  41224  mapdh8ab  41250  mapdh8ad  41252  mapdh8e  41257  mapdh9a  41262  mapdh9aOLDN  41263  hdmap1l6a  41282  hdmap1l6d  41286  hdmap1l6e  41287  hdmap1l6h  41290  hdmap1eulem  41295  hdmap1eulemOLDN  41296  hdmapval0  41306  hdmapeveclem  41307  hdmapval3lemN  41310  hdmap10lem  41312  hdmap11lem1  41314  hdmaprnlem3N  41323  hdmaprnlem9N  41330  hdmaprnlem3eN  41331  fzne2d  41451  lcmineqlem11  41510  3lexlogpow5ineq1  41525  3lexlogpow5ineq2  41526  3lexlogpow5ineq4  41527  3lexlogpow5ineq3  41528  3lexlogpow2ineq1  41529  3lexlogpow2ineq2  41530  3lexlogpow5ineq5  41531  aks4d1lem1  41533  dvrelog2b  41537  dvrelogpow2b  41539  aks4d1p1p3  41540  aks4d1p1p2  41541  aks4d1p1p4  41542  aks4d1p1p6  41544  aks4d1p1p7  41545  aks4d1p1p5  41546  aks4d1p1  41547  aks4d1p2  41548  aks4d1p3  41549  aks4d1p5  41551  aks4d1p6  41552  aks4d1p7d1  41553  aks4d1p7  41554  aks4d1p8d3  41557  aks4d1p8  41558  aks4d1p9  41559  fldhmf1  41561  aks6d1c2p2  41590  hashscontpow  41593  aks6d1c3  41594  aks6d1c5lem2  41609  2np3bcnp1  41616  2ap1caineq  41617  sticksstones1  41618  sticksstones2  41619  sticksstones10  41627  sticksstones12a  41629  sticksstones12  41630  sticksstones22  41640  aks6d1c6lem4  41645  aks6d1c7lem2  41653  metakunt7  41663  metakunt12  41668  metakunt22  41678  xppss12  41717  mhpind  41827  jm2.26lem3  42422  rpnnen3lem  42452  rpnnen3  42453  imo72b2lem0  43595  imo72b2lem2  43597  imo72b2  43602  mnuprdlem1  43709  bcc0  43777  chordthmALT  44372  fnchoice  44391  refsum2cnlem1  44399  xrleneltd  44705  xrltned  44739  infleinf  44754  reclt0  44773  icoiccdif  44909  ressiooinf  44942  limcresiooub  45030  limcleqr  45032  limclner  45039  climxrre  45138  icccncfext  45275  cncfiooiccre  45283  dvnxpaek  45330  stoweidlem43  45431  stirlinglem5  45466  stirlinglem7  45468  dirkercncflem1  45491  fourierdlem24  45519  fourierdlem32  45527  fourierdlem33  45528  fourierdlem34  45529  fourierdlem35  45530  fourierdlem46  45540  fourierdlem48  45542  fourierdlem49  45543  fourierdlem64  45558  fourierdlem65  45559  fourierdlem74  45568  fourierdlem76  45570  fourierdlem79  45573  fourierdlem81  45575  fourierdlem91  45585  fourierdlem102  45596  fourierdlem114  45608  etransclem15  45637  etransclem24  45646  sge0rpcpnf  45809  sge0isum  45815  pimrecltpos  46096  pimiooltgt  46098  setsnidel  46717  odz2prm2pw  46903  fmtnoprmfac1lem  46904  fmtnoprmfac1  46905  fmtnoprmfac2  46907  lighneallem1  46945  lighneallem3  46947  perfectALTVlem2  47062  nnsgrpnmnd  47240  lvecpsslmod  47575  affinecomb1  47775  affinecomb2  47776  1subrec1sub  47778  rrx2plord2  47795  line  47805  rrxline  47807  eenglngeehlnmlem2  47811  rrx2vlinest  47814  line2xlem  47826  2itscp  47854