Theorem necomd 2999

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

Syntax hints:   → wi 4   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731  df-ne 2944

This theorem is referenced by:  difsnb  4736  0nelop  5403  xpdifid  6059  difsnen  8771  fofinf1o  8999  en2eleq  9670  en2other2  9671  ackbij1lem15  9896  infpssrlem5  9969  fin23lem24  9984  fin23lem31  10005  isf32lem9  10023  canthnumlem  10310  canthp1lem2  10315  npomex  10658  ltned  11016  lt0ne0  11346  recgt0  11726  zneo  12308  xrltne  12801  supxrbnd  12966  flltnz  13434  seqf1olem1  13665  nn0opthi  13887  hashtpg  14102  hashge3el3dif  14103  cats1un  14337  sumtp  15364  geoserg  15481  geolim  15485  geolim2  15486  tanadd  15779  ruclem6  15847  ruclem7  15848  isprm2lem  16289  isprm5  16315  oddprm  16414  pcmpt  16496  cshwshashlem3  16702  resshom  17021  ressco  17022  mrissmrcd  17241  rescco  17437  estrres  17747  smndex2dnrinv  18444  pmtrprfv  18951  symggen  18968  dprdcntz  19501  dprdres  19521  ablfac1b  19563  lbspss  20234  lspsnnecom  20271  lspindp2l  20286  lspindp2  20287  islbs3  20307  lbsextlem4  20313  sralemOLD  20330  lidlnz  20387  01eq0ring  20431  uvcf1  20884  frlmup2  20891  psrridm  21058  coe1tmfv2  21331  coe1tmmul  21333  dmatmul  21529  mdetralt  21640  mdetunilem2  21645  mdetunilem6  21649  mdetunilem7  21650  maducoeval2  21672  madurid  21676  fvmptnn04ifa  21882  en2top  22018  cmpfi  22442  snfil  22898  tsmsfbas  23162  zcld  23857  iccpnfhmeo  23989  xrhmeo  23990  evth  24003  minveclem3b  24472  i1fres  24750  dvcnvlem  25020  ig1peu  25216  ig1pdvds  25221  aaliou3lem9  25390  taylthlem2  25413  abelthlem2  25471  abelthlem7  25477  cos02pilt1  25562  tanregt0  25575  logcj  25641  argimgt0  25647  dvloglem  25683  logf1o2  25685  logbrec  25812  ang180lem1  25839  ang180lem2  25840  ang180lem3  25841  ang180lem4  25842  ang180lem5  25843  ang180  25844  isosctrlem3  25850  ssscongptld  25852  affineequivne  25857  angpieqvdlem  25858  angpieqvdlem2  25859  angpieqvd  25861  chordthmlem  25862  chordthmlem2  25863  chordthm  25867  asinneg  25916  ppiltx  26206  perfectlem2  26258  lgsneg  26349  lgsqr  26379  lgseisenlem4  26406  lgsquadlem1  26408  lgsquadlem3  26410  lgsquad2  26414  2lgsoddprm  26444  dchrisum0flblem1  26536  tgbtwnouttr  26737  tgifscgr  26748  tgcgrxfr  26758  tglngval  26791  tgfscgr  26808  tgbtwnconn1lem3  26814  tgbtwnconn3  26817  legtrid  26831  hltr  26850  hlbtwn  26851  btwnhl1  26852  btwnhl  26854  hlcgrex  26856  hlcgreulem  26857  lncom  26862  tgisline  26867  tglineeltr  26871  tglineelsb2  26872  tglinecom  26875  tglinethru  26876  ncolncol  26886  coltr  26887  coltr3  26888  symquadlem  26929  midexlem  26932  ragcol  26939  ragcgr  26947  perpneq  26954  footexALT  26958  footexlem1  26959  footexlem2  26960  foot  26962  footne  26963  colperpexlem3  26972  mideulem2  26974  opphllem  26975  midex  26977  opphllem1  26987  opphllem2  26988  opphllem3  26989  opphllem4  26990  opphllem5  26991  opphllem6  26992  outpasch  26995  hlpasch  26996  lnopp2hpgb  27003  colhp  27010  lmieu  27024  hypcgrlem1  27039  hypcgrlem2  27040  lnperpex  27043  trgcopy  27044  trgcopyeulem  27045  iscgra1  27050  cgrane2  27053  cgrane3  27054  cgrane4  27055  cgracgr  27058  cgraid  27059  cgraswap  27060  cgrcgra  27061  cgracom  27062  cgratr  27063  flatcgra  27064  cgraswaplr  27065  cgracol  27068  dfcgra2  27070  sacgr  27071  oacgr  27072  acopy  27073  acopyeu  27074  leagne2  27090  leagne3  27091  cgrg3col4  27093  tgsas1  27094  tgsas2  27096  tgasa1  27098  ttgcontlem1  27130  cchhllemOLD  27133  brbtwn2  27151  axlowdimlem15  27202  axlowdimlem16  27203  axcontlem8  27217  upgrex  27340  edglnl  27391  umgrvad2edg  27458  nbupgr  27589  nbumgrvtx  27591  nbgr2vtx1edg  27595  nbuhgr2vtx1edgb  27597  nbupgrres  27609  cplgr3v  27680  cusgrexilem2  27687  usgredgsscusgredg  27704  1hegrvtxdg1r  27753  1egrvtxdg1r  27755  1egrvtxdg0  27756  pthdadjvtx  27974  pthdlem2lem  28011  wspniunwspnon  28164  umgr2cwwk2dif  28304  3pthdlem1  28404  uhgr3cyclex  28422  upgr4cycl4dv4e  28425  frgr3v  28515  1to3vfriswmgr  28520  frgrwopreglem5a  28551  frgrwopreglem3  28554  frgrhash2wsp  28572  staddi  30484  unidifsnne  30760  coprprop  30909  pmtrcnel  31235  pmtrcnel2  31236  psgnfzto1stlem  31244  cycpmco2lem1  31270  cycpmco2  31277  cyc2fvx  31278  cyc3co2  31284  cycpmrn  31287  tocyccntz  31288  cyc3evpm  31294  cyc3genpmlem  31295  ornglmullt  31383  orngrmullt  31384  orngmullt  31385  ofldlt1  31389  ofldchr  31390  isarchiofld  31393  qsidomlem2  31506  mxidlnzr  31516  1smat1  31631  submateqlem1  31634  madjusmdetlem2  31655  ordtconnlem1  31751  esumrnmpt2  31911  cntnevol  32071  signstfveq0a  32430  repr0  32466  reprlt  32474  reprinfz1  32477  cusgredgex  32958  2cycl2d  32976  acycgr1v  32986  derangenlem  33008  subfacp1lem1  33016  subfacp1lem3  33019  subfacp1lem5  33021  fmlasucdisj  33236  noseponlem  33769  nosep1o  33786  nosep2o  33787  nosupbnd2lem1  33820  noinfbnd2lem1  33835  noetasuplem4  33841  noetainflem4  33845  slerec  33915  dfrdg4  34155  ifscgr  34248  cgrxfr  34259  btwnconn1lem8  34298  btwnconn3  34307  segcon2  34309  broutsideof3  34330  outsideoftr  34333  outsideofeq  34334  outsideofeu  34335  lineunray  34351  lineelsb2  34352  linethru  34357  unbdqndv2lem2  34592  knoppndvlem1  34594  knoppndvlem2  34595  knoppndvlem7  34600  knoppndvlem14  34607  bj-bary1lem  35384  bj-bary1lem1  35385  bj-bary1  35386  finxpreclem2  35467  finxp1o  35469  finxpreclem6  35473  fin2solem  35669  poimirlem9  35692  poimirlem15  35698  poimirlem20  35703  poimirlem24  35707  poimirlem25  35708  poimirlem27  35710  itg2addnclem2  35735  ftc1cnnc  35755  heibor1lem  35873  maxidln0  36109  lshpnelb  36904  lsatssn0  36922  lsatcv0  36951  lsat0cv  36953  lsatexch1  36966  l1cvat  36975  atlen0  37230  cvlsupr2  37263  atcvrj2b  37352  2atlt  37359  atbtwn  37366  3noncolr2  37369  4noncolr3  37373  3dimlem3  37381  3dimlem3OLDN  37382  3dimlem4  37384  3dimlem4OLDN  37385  3dim2  37388  1cvratex  37393  1cvrat  37396  ps-1  37397  ps-2  37398  hlatexch4  37401  3atlem4  37406  3atlem6  37408  4atlem0ae  37514  4atlem0be  37515  dalemccnedd  37607  dalemrotps  37611  dalem21  37614  dalem23  37616  dalem27  37619  dalem41  37633  dalem44  37636  dalem54  37646  lnatexN  37699  lnjatN  37700  llnexchb2lem  37788  llnexchb2  37789  lhpn0  37924  lhpexle3lem  37931  lhpmatb  37951  4atexlemswapqr  37983  4atexlemc  37989  4atexlemnclw  37990  4atexlemcnd  37992  4atexlemex4  37993  4atexlemex6  37994  4atex  37996  trlat  38089  trlval4  38108  cdlemc5  38115  cdlemd4  38121  cdlemd7  38124  cdlemd9  38126  cdleme0e  38137  cdleme3b  38149  cdleme3c  38150  cdleme3e  38152  cdleme3h  38155  cdleme7aa  38162  cdleme7e  38167  cdleme7ga  38168  cdleme9  38173  cdleme11c  38181  cdleme11e  38183  cdleme11fN  38184  cdleme11h  38186  cdleme11j  38187  cdleme11k  38188  cdleme15b  38195  cdleme15c  38196  cdleme17c  38208  cdleme18b  38212  cdlemesner  38216  cdleme20zN  38221  cdleme19c  38225  cdleme19d  38226  cdleme19e  38227  cdleme20m  38243  cdleme21a  38245  cdleme21b  38246  cdleme21c  38247  cdleme22f2  38267  cdleme28b  38291  cdleme36a  38380  cdleme36m  38381  cdleme41sn4aw  38395  cdleme43bN  38410  cdleme43dN  38412  cdleme46f2g2  38413  cdleme46f2g1  38414  cdleme4gfv  38427  cdlemeg46nlpq  38437  cdlemeg46req  38449  cdlemeg46fgN  38454  cdlemf1  38481  cdlemg8b  38548  cdlemg9a  38552  cdlemg12g  38569  cdlemg12  38570  cdlemg13a  38571  cdlemg17pq  38592  cdlemg18a  38598  cdlemg18c  38600  cdlemg19a  38603  cdlemg19  38604  cdlemg21  38606  cdlemg31b0N  38614  cdlemg31b0a  38615  cdlemg31c  38619  cdlemg33b0  38621  cdlemg33c0  38622  trlcone  38648  cdlemg42  38649  cdlemg44a  38651  cdlemg46  38655  cdlemh1  38735  cdlemh2  38736  cdlemh  38737  cdlemj3  38743  cdlemk3  38753  cdlemki  38761  cdlemksv2  38767  cdlemk12  38770  cdlemk14  38774  cdlemk15  38775  cdlemk7u  38790  cdlemk11u  38791  cdlemk12u  38792  cdlemk21N  38793  cdlemk20  38794  cdlemk22  38813  cdlemk26-3  38826  cdlemk27-3  38827  cdlemk28-3  38828  cdlemkfid3N  38845  cdlemk11ta  38849  cdlemk47  38869  cdlemk54  38878  dia2dimlem1  38984  dochsat  39303  dochshpncl  39304  lclkrlem2b  39428  lcfrlem21  39483  baerlem5amN  39636  baerlem5bmN  39637  baerlem5abmN  39638  mapdindp4  39643  mapdheq2  39649  mapdheq2biN  39650  mapdh6aN  39655  mapdh6dN  39659  mapdh6eN  39660  mapdh6hN  39663  mapdh7eN  39668  mapdh7dN  39670  mapdh7fN  39671  mapdh8ab  39697  mapdh8ad  39699  mapdh8e  39704  mapdh9a  39709  mapdh9aOLDN  39710  hdmap1l6a  39729  hdmap1l6d  39733  hdmap1l6e  39734  hdmap1l6h  39737  hdmap1eulem  39742  hdmap1eulemOLDN  39743  hdmapval0  39753  hdmapeveclem  39754  hdmapval3lemN  39757  hdmap10lem  39759  hdmap11lem1  39761  hdmaprnlem3N  39770  hdmaprnlem9N  39777  hdmaprnlem3eN  39778  fzne2d  39896  lcmineqlem11  39954  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow5ineq4  39971  3lexlogpow5ineq3  39972  3lexlogpow2ineq1  39973  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  dvrelog2b  39980  dvrelogpow2b  39982  aks4d1p1p3  39983  aks4d1p1p2  39984  aks4d1p1p4  39985  aks4d1p1p6  39987  aks4d1p1p7  39988  aks4d1p1p5  39989  aks4d1p1  39990  aks4d1p2  39991  aks4d1p3  39992  aks4d1p5  39994  aks4d1p6  39995  aks4d1p7d1  39996  aks4d1p7  39997  2np3bcnp1  40000  2ap1caineq  40001  sticksstones1  40002  sticksstones2  40003  sticksstones10  40011  sticksstones12a  40013  sticksstones12  40014  sticksstones22  40024  metakunt7  40031  metakunt12  40036  metakunt22  40046  xppss12  40102  mhpind  40178  jm2.26lem3  40711  rpnnen3lem  40741  rpnnen3  40742  imo72b2lem0  41638  imo72b2lem2  41640  imo72b2  41645  mnuprdlem1  41752  bcc0  41820  chordthmALT  42415  fnchoice  42434  refsum2cnlem1  42442  xrleneltd  42725  xrltned  42759  infleinf  42774  reclt0  42794  icoiccdif  42925  ressiooinf  42958  limcresiooub  43046  limcleqr  43048  limclner  43055  climxrre  43154  icccncfext  43291  cncfiooiccre  43299  dvnxpaek  43346  stoweidlem43  43447  stirlinglem5  43482  stirlinglem7  43484  dirkercncflem1  43507  fourierdlem24  43535  fourierdlem32  43543  fourierdlem33  43544  fourierdlem34  43545  fourierdlem35  43546  fourierdlem46  43556  fourierdlem48  43558  fourierdlem49  43559  fourierdlem64  43574  fourierdlem65  43575  fourierdlem74  43584  fourierdlem76  43586  fourierdlem79  43589  fourierdlem81  43591  fourierdlem91  43601  fourierdlem102  43612  fourierdlem114  43624  etransclem15  43653  etransclem24  43662  sge0rpcpnf  43822  sge0isum  43828  pimrecltpos  44106  pimiooltgt  44108  setsnidel  44690  odz2prm2pw  44876  fmtnoprmfac1lem  44877  fmtnoprmfac1  44878  fmtnoprmfac2  44880  lighneallem1  44918  lighneallem3  44920  perfectALTVlem2  45035  nnsgrpnmnd  45233  nrhmzr  45292  lvecpsslmod  45709  affinecomb1  45909  affinecomb2  45910  1subrec1sub  45912  rrx2plord2  45929  line  45939  rrxline  45941  eenglngeehlnmlem2  45945  rrx2vlinest  45948  line2xlem  45960  2itscp  45988